Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mtoi | Unicode version |
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
Ref | Expression |
---|---|
mtoi.1 | |
mtoi.2 |
Ref | Expression |
---|---|
mtoi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtoi.1 | . . 3 | |
2 | 1 | a1i 9 | . 2 |
3 | mtoi.2 | . 2 | |
4 | 2, 3 | mtod 653 | 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: mtbii 664 mtbiri 665 pwnss 4132 nsuceq0g 4390 abnex 4419 reg2exmidlema 4505 ordsuc 4534 onnmin 4539 ssnel 4540 ordtri2or2exmid 4542 ontri2orexmidim 4543 reg3exmidlemwe 4550 acexmidlemab 5830 reldmtpos 6212 dmtpos 6215 2pwuninelg 6242 onunsnss 6873 snon0 6892 nninfisol 7088 exmidomni 7097 pr2ne 7139 ltexprlemdisj 7538 recexprlemdisj 7562 caucvgprlemnkj 7598 caucvgprprlemnkltj 7621 caucvgprprlemnkeqj 7622 caucvgprprlemnjltk 7623 inelr 8473 rimul 8474 recgt0 8736 zfz1iso 10740 isprm2 12028 nprmdvds1 12051 divgcdodd 12054 coprm 12055 coseq0q4123 13302 pwle2 13719 exmid1stab 13721 nninfalllem1 13729 nninfall 13730 nninfsellemqall 13736 |
Copyright terms: Public domain | W3C validator |