Thank you! Sorry I just deleted my post because I realized the answer myself.
Op dinsdag 15 augustus 2023 om 20:51:38 UTC+2 schreef Thierry Arnoux: > 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/3456b89a-4e60-4724-880a-6024b655f5fbn%40googlegroups.com.
