That's the irrefutability of the law of the excluded middle, and yes it's probably the most difficult of the regular exercises. Here you go
https://i.imgur.com/WIPJE8s.png Best regards, Antony On Tue, Jun 18, 2019 at 4:01 PM Tony <[email protected]> wrote: > How do I prove the last one in session 4: (A∨(A→⊥)→⊥)→⊥ ? > On Monday, April 1, 2019 at 3:00:00 AM UTC+2, David A. Wheeler wrote: >> >> FYI: I've just learned about The Incredible Proof Machine: >> >> http://incredible.pm/ >> >> -- > 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/65ae121f-beb9-4800-939e-93a20b0d3696%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/65ae121f-beb9-4800-939e-93a20b0d3696%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/CAJ48g%2BC-Wq4KGPDny%2BsbrgsFNx7Be301AEYJJ5-6aUEfJNjHAQ%40mail.gmail.com.
