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 321 | . 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
3 | sylnbi.2 | . 2 ⊢ (¬ 𝜓 → 𝜒) | |
4 | 2, 3 | sylbi 218 | 1 ⊢ (¬ 𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: sylnbir 332 reuun2 4283 opswap 6079 iotanul 6326 riotaund 7142 ndmovcom 7324 suppssov1 7851 suppssfv 7855 brtpos 7890 snnen2o 8695 ranklim 9261 rankuni 9280 ituniiun 9832 hashprb 13746 1mavmul 21085 nonbooli 29355 disjunsn 30272 bj-rest10b 34274 disjrnmpt2 41325 ndmaovcl 43279 ndmaovcom 43281 lindslinindsimp1 44440 |
Copyright terms: Public domain | W3C validator |