Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylnib | GIF version |
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnib.1 | ⊢ (𝜑 → ¬ 𝜓) |
sylnib.2 | ⊢ (𝜓 ↔ 𝜒) |
Ref | Expression |
---|---|
sylnib | ⊢ (𝜑 → ¬ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnib.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | sylnib.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
3 | 2 | a1i 9 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
4 | 1, 3 | mtbid 661 | 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 603 ax-in2 604 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnibr 666 neqcomd 2144 inssdif0im 3430 undifexmid 4117 ordtriexmidlem2 4436 dmsn0el 5008 fidifsnen 6764 ctssdccl 6996 ltpopr 7403 caucvgprprlemnbj 7501 xrlttri3 9583 fzneuz 9881 iseqf1olemqcl 10259 iseqf1olemnab 10261 iseqf1olemab 10262 exp3val 10295 pwle2 13193 |
Copyright terms: Public domain | W3C validator |