![]() |
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 588 | 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 598 mtbiri 599 pwnss 3903 nsuceq0g 4121 ordsuc 4241 onnmin 4244 ssnel 4245 onpsssuc 4247 acexmidlemab 5449 reldmtpos 5809 dmtpos 5812 2pwuninelg 5839 ltexprlemdisj 6580 recexprlemdisj 6602 caucvgprlemnkj 6637 inelr 7368 rimul 7369 recgt0 7597 |
Copyright terms: Public domain | W3C validator |