![]() |
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 664 |
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 615 ax-in2 616 |
This theorem is referenced by: mtbii 675 mtbiri 676 pwnss 4189 exmid1stab 4238 nsuceq0g 4450 abnex 4479 reg2exmidlema 4567 ordsuc 4596 onnmin 4601 ssnel 4602 ordtri2or2exmid 4604 ontri2orexmidim 4605 reg3exmidlemwe 4612 acexmidlemab 5913 reldmtpos 6308 dmtpos 6311 2pwuninelg 6338 onunsnss 6975 snon0 6996 nninfisol 7194 exmidomni 7203 pr2ne 7254 ltexprlemdisj 7668 recexprlemdisj 7692 caucvgprlemnkj 7728 caucvgprprlemnkltj 7751 caucvgprprlemnkeqj 7752 caucvgprprlemnjltk 7753 inelr 8605 rimul 8606 recgt0 8871 zfz1iso 10915 isprm2 12258 nprmdvds1 12281 divgcdodd 12284 coprm 12285 coseq0q4123 15010 lgsquad2lem2 15239 pwle2 15559 nninfalllem1 15568 nninfall 15569 nninfsellemqall 15575 |
Copyright terms: Public domain | W3C validator |