![]() |
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 157 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
4 | 1, 3 | mtod 653 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnib 666 eqneltrrd 2237 neleqtrd 2238 eueq3dc 2862 efrirr 4283 fidcenumlemrks 6849 nqnq0pi 7270 zdclt 9152 xleaddadd 9700 frec2uzf1od 10210 expnegap0 10332 bcval5 10541 zfz1isolemiso 10614 seq3coll 10617 fisumss 11193 rpdvds 11816 oddpwdclemodd 11886 pwle2 13366 |
Copyright terms: Public domain | W3C validator |