![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtoi | GIF 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: ¬ wn 3 → wi 4 |
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 4177 exmid1stab 4226 nsuceq0g 4436 abnex 4465 reg2exmidlema 4551 ordsuc 4580 onnmin 4585 ssnel 4586 ordtri2or2exmid 4588 ontri2orexmidim 4589 reg3exmidlemwe 4596 acexmidlemab 5890 reldmtpos 6278 dmtpos 6281 2pwuninelg 6308 onunsnss 6945 snon0 6965 nninfisol 7161 exmidomni 7170 pr2ne 7221 ltexprlemdisj 7635 recexprlemdisj 7659 caucvgprlemnkj 7695 caucvgprprlemnkltj 7718 caucvgprprlemnkeqj 7719 caucvgprprlemnjltk 7720 inelr 8571 rimul 8572 recgt0 8837 zfz1iso 10853 isprm2 12149 nprmdvds1 12172 divgcdodd 12175 coprm 12176 coseq0q4123 14712 pwle2 15207 nninfalllem1 15216 nninfall 15217 nninfsellemqall 15223 |
Copyright terms: Public domain | W3C validator |