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 589 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 544 ax-in2 545 |
This theorem is referenced by: mtbii 599 mtbiri 600 pwnss 3912 nsuceq0g 4155 reg2exmidlema 4259 ordsuc 4287 onnmin 4292 ssnel 4293 onpsssuc 4295 ordtri2or2exmid 4296 reg3exmidlemwe 4303 acexmidlemab 5506 reldmtpos 5868 dmtpos 5871 2pwuninelg 5898 onunsnss 6355 snon0 6356 ltexprlemdisj 6704 recexprlemdisj 6728 caucvgprlemnkj 6764 caucvgprprlemnkltj 6787 caucvgprprlemnkeqj 6788 caucvgprprlemnjltk 6789 inelr 7575 rimul 7576 recgt0 7816 |
Copyright terms: Public domain | W3C validator |