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 637 | 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 588 ax-in2 589 |
This theorem is referenced by: mtbii 648 mtbiri 649 pwnss 4053 nsuceq0g 4310 abnex 4338 reg2exmidlema 4419 ordsuc 4448 onnmin 4453 ssnel 4454 ordtri2or2exmid 4456 reg3exmidlemwe 4463 acexmidlemab 5736 reldmtpos 6118 dmtpos 6121 2pwuninelg 6148 onunsnss 6773 snon0 6792 exmidomni 6982 pr2ne 7016 ltexprlemdisj 7382 recexprlemdisj 7406 caucvgprlemnkj 7442 caucvgprprlemnkltj 7465 caucvgprprlemnkeqj 7466 caucvgprprlemnjltk 7467 inelr 8314 rimul 8315 recgt0 8576 zfz1iso 10552 isprm2 11725 nprmdvds1 11747 divgcdodd 11748 coprm 11749 coseq0q4123 12842 pwle2 13120 exmid1stab 13122 nninfalllem1 13130 nninfall 13131 nninfsellemqall 13138 |
Copyright terms: Public domain | W3C validator |