![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylnibr | GIF version |
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting an consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnibr.1 | ⊢ (𝜑 → ¬ 𝜓) |
sylnibr.2 | ⊢ (𝜒 ↔ 𝜓) |
Ref | Expression |
---|---|
sylnibr | ⊢ (𝜑 → ¬ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnibr.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | sylnibr.2 | . . 3 ⊢ (𝜒 ↔ 𝜓) | |
3 | 2 | bicomi 123 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | sylnib 601 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: rexnalim 2317 nssr 3003 difdif 3069 unssin 3176 inssun 3177 undif3ss 3198 ssdif0im 3286 prneimg 3545 iundif2ss 3722 nssssr 3958 pofun 4049 frirrg 4087 regexmidlem1 4258 nndifsnid 6080 fidifsnid 6332 addnqprlemfl 6657 addnqprlemfu 6658 mulnqprlemfl 6673 mulnqprlemfu 6674 cauappcvgprlemladdru 6754 caucvgprprlemaddq 6806 fzpreddisj 8933 |
Copyright terms: Public domain | W3C validator |