Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mto | Unicode version |
Description: The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Ref | Expression |
---|---|
mto.1 | |
mto.2 |
Ref | Expression |
---|---|
mto |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mto.2 | . 2 | |
2 | mto.1 | . . 3 | |
3 | 2 | a1i 9 | . 2 |
4 | 1, 3 | pm2.65i 634 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 609 ax-in2 610 |
This theorem is referenced by: mtbi 665 pm3.2ni 808 pm5.16 823 intnan 924 intnanr 925 equidqe 1525 nexr 1685 ru 2954 neldifsn 3713 nvel 4122 nlim0 4379 snnex 4433 onprc 4536 dtruex 4543 ordsoexmid 4546 nprrel 4656 0xp 4691 iprc 4879 son2lpi 5007 nfunv 5231 0fv 5531 canth 5807 acexmidlema 5844 acexmidlemb 5845 acexmidlemab 5847 mpo0 5923 php5dom 6841 fi0 6952 pw1ne1 7206 pw1ne3 7207 sucpw1nel3 7210 3nelsucpw1 7211 0nnq 7326 0npr 7445 1ne0sr 7728 pnfnre 7961 mnfnre 7962 ine0 8313 inelr 8503 nn0nepnf 9206 1nuz2 9565 0nrp 9646 inftonninf 10397 eirr 11741 odd2np1 11832 n2dvds1 11871 1nprm 12068 structcnvcnv 12432 fvsetsid 12450 0g0 12630 0ntop 12799 topnex 12880 bj-nvel 13932 pwle2 14031 exmidsbthrlem 14054 trirec0xor 14077 |
Copyright terms: Public domain | W3C validator |