On 15/08/2023 20:40, Jeroen van Rensen wrote:
Hi, and what about when you do have both T and Ti? Do you know how I then should go to Td?
That's the case where you would use the "weak deduction theorem", ~dedth <https://us.metamath.org/mpeuni/dedth.html>. The comment in dedth has a short explanation, and this is described in more details in https://us.metamath.org/mpeuni/mmdeduction.html. The first example I found in set.mm is ~bnd2d <https://us.metamath.org/mpeuni/bnd2d.html>, which is derived from bnd2 using this technique. BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6c10d6a1-8b18-ed36-cad3-f017b0fa88aa%40gmx.net.
