![]() |
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 322 | . 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
3 | sylnbi.2 | . 2 ⊢ (¬ 𝜓 → 𝜒) | |
4 | 2, 3 | sylbi 219 | 1 ⊢ (¬ 𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 |
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 209 |
This theorem is referenced by: sylnbir 333 reuun2 4288 opswap 6088 iotanul 6335 riotaund 7155 ndmovcom 7337 suppssov1 7864 suppssfv 7868 brtpos 7903 snnen2o 8709 ranklim 9275 rankuni 9294 ituniiun 9846 hashprb 13761 1mavmul 21159 nonbooli 29430 disjunsn 30346 bj-rest10b 34382 disjrnmpt2 41456 ndmaovcl 43409 ndmaovcom 43411 lindslinindsimp1 44519 |
Copyright terms: Public domain | W3C validator |