![]() |
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 131 | . 2 ⊢ (𝜓 ↔ 𝜒) |
4 | 1, 3 | sylnib 642 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: rexnalim 2386 nssr 3107 difdif 3148 unssin 3262 inssun 3263 undif3ss 3284 ssdif0im 3374 dcun 3420 prneimg 3648 iundif2ss 3825 nssssr 4082 pofun 4172 frirrg 4210 regexmidlem1 4386 dcdifsnid 6330 unfidisj 6739 fidcenumlemrks 6769 difinfsn 6900 addnqprlemfl 7268 addnqprlemfu 7269 mulnqprlemfl 7284 mulnqprlemfu 7285 cauappcvgprlemladdru 7365 caucvgprprlemaddq 7417 fzpreddisj 9692 pw2dvdslemn 11635 pwtrufal 12777 nninfsellemsuc 12792 |
Copyright terms: Public domain | W3C validator |