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 629 | 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 604 ax-in2 605 |
This theorem is referenced by: mtbi 660 pm3.2ni 803 pm5.16 814 intnan 915 intnanr 916 equidqe 1512 nexr 1672 ru 2936 neldifsn 3691 nvel 4100 nlim0 4357 snnex 4411 onprc 4514 dtruex 4521 ordsoexmid 4524 nprrel 4634 0xp 4669 iprc 4857 son2lpi 4985 nfunv 5206 0fv 5506 canth 5781 acexmidlema 5818 acexmidlemb 5819 acexmidlemab 5821 mpo0 5894 php5dom 6811 fi0 6922 pw1ne1 7167 pw1ne3 7168 sucpw1nel3 7171 3nelsucpw1 7172 0nnq 7287 0npr 7406 1ne0sr 7689 pnfnre 7922 mnfnre 7923 ine0 8274 inelr 8464 nn0nepnf 9167 1nuz2 9523 0nrp 9603 inftonninf 10350 eirr 11687 odd2np1 11777 n2dvds1 11816 1nprm 12007 structcnvcnv 12302 fvsetsid 12320 0ntop 12501 topnex 12582 bj-nnst 13428 bj-nvel 13569 pwle2 13667 exmidsbthrlem 13690 trirec0xor 13713 |
Copyright terms: Public domain | W3C validator |