![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtbid | GIF version |
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.) |
Ref | Expression |
---|---|
mtbid.min | ⊢ (𝜑 → ¬ 𝜓) |
mtbid.maj | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
mtbid | ⊢ (𝜑 → ¬ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbid.min | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | mtbid.maj | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 2 | biimprd 158 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
4 | 1, 3 | mtod 664 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: sylnib 677 eqneltrrd 2286 neleqtrd 2287 eueq3dc 2926 efrirr 4371 fidcenumlemrks 6982 nqnq0pi 7467 zdclt 9360 xleaddadd 9917 frec2uzf1od 10437 expnegap0 10559 bcval5 10775 zfz1isolemiso 10851 seq3coll 10854 fisumss 11432 fprodssdc 11630 rpdvds 12131 oddpwdclemodd 12204 pceq0 12354 pcmpt 12375 lgseisenlem1 14908 2sqlem8a 14927 2sqlem8 14928 pwle2 15207 |
Copyright terms: Public domain | W3C validator |