![]() |
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 672 | 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 614 ax-in2 615 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: sylnibr 677 neqcomd 2182 inssdif0im 3490 undifexmid 4193 ordtriexmidlem2 4519 dmsn0el 5098 fidifsnen 6869 ctssdccl 7109 nninfwlpoimlemginf 7173 onntri35 7235 onntri45 7239 2omotaplemap 7255 exmidapne 7258 ltpopr 7593 caucvgprprlemnbj 7691 xrlttri3 9795 fzneuz 10098 iseqf1olemqcl 10483 iseqf1olemnab 10485 iseqf1olemab 10486 exp3val 10519 pwle2 14630 |
Copyright terms: Public domain | W3C validator |