![]() |
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 624 | 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 579 ax-in2 580 |
This theorem is referenced by: mtbii 634 mtbiri 635 pwnss 3994 nsuceq0g 4245 reg2exmidlema 4350 ordsuc 4379 onnmin 4384 ssnel 4385 ordtri2or2exmid 4387 reg3exmidlemwe 4394 acexmidlemab 5646 reldmtpos 6018 dmtpos 6021 2pwuninelg 6048 onunsnss 6627 snon0 6645 exmidomni 6798 pr2ne 6820 ltexprlemdisj 7165 recexprlemdisj 7189 caucvgprlemnkj 7225 caucvgprprlemnkltj 7248 caucvgprprlemnkeqj 7249 caucvgprprlemnjltk 7250 inelr 8061 rimul 8062 recgt0 8311 zfz1iso 10246 isprm2 11377 nprmdvds1 11399 divgcdodd 11400 coprm 11401 nninfalllem1 11899 nninfall 11900 nninfsellemqall 11907 |
Copyright terms: Public domain | W3C validator |