![]() |
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 663 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 614 ax-in2 615 |
This theorem is referenced by: mtbii 674 mtbiri 675 pwnss 4159 exmid1stab 4208 nsuceq0g 4418 abnex 4447 reg2exmidlema 4533 ordsuc 4562 onnmin 4567 ssnel 4568 ordtri2or2exmid 4570 ontri2orexmidim 4571 reg3exmidlemwe 4578 acexmidlemab 5868 reldmtpos 6253 dmtpos 6256 2pwuninelg 6283 onunsnss 6915 snon0 6934 nninfisol 7130 exmidomni 7139 pr2ne 7190 ltexprlemdisj 7604 recexprlemdisj 7628 caucvgprlemnkj 7664 caucvgprprlemnkltj 7687 caucvgprprlemnkeqj 7688 caucvgprprlemnjltk 7689 inelr 8539 rimul 8540 recgt0 8805 zfz1iso 10816 isprm2 12111 nprmdvds1 12134 divgcdodd 12137 coprm 12138 coseq0q4123 14186 pwle2 14668 nninfalllem1 14677 nninfall 14678 nninfsellemqall 14684 |
Copyright terms: Public domain | W3C validator |