In practice it's rarely used, as we state the majority of theorems either in closed form or in deduction form, but from a theoretical/learning standpoint it's interesting to know it's possible - and that's why it will be of interest to you!
Actually I see many theorems using it are from the deprecated Hibert Space Explorer (parts 18 and 19). On 15/08/2023 20:53, Jeroen van Rensen wrote:
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 <http://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 <https://groups.google.com/d/msgid/metamath/3456b89a-4e60-4724-880a-6024b655f5fbn%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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/363847d4-5191-17c9-ae0f-c007790bf481%40gmx.net.
