![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylnbi | Structured version Visualization version GIF version |
Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnbi.1 | ⊢ (𝜑 ↔ 𝜓) |
sylnbi.2 | ⊢ (¬ 𝜓 → 𝜒) |
Ref | Expression |
---|---|
sylnbi | ⊢ (¬ 𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnbi.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | notbii 312 | . 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
3 | sylnbi.2 | . 2 ⊢ (¬ 𝜓 → 𝜒) | |
4 | 2, 3 | sylbi 209 | 1 ⊢ (¬ 𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 199 |
This theorem is referenced by: sylnbir 323 reuun2 4136 opswap 5876 iotanul 6114 riotaund 6919 ndmovcom 7098 suppssov1 7609 suppssfv 7613 brtpos 7643 snnen2o 8437 ranklim 9004 rankuni 9023 cdacomen 9338 ituniiun 9579 hashprb 13499 1mavmul 20759 nonbooli 29082 disjunsn 29970 bj-rest10b 33615 ndmaovcl 42244 ndmaovcom 42246 lindslinindsimp1 43261 |
Copyright terms: Public domain | W3C validator |