![]() |
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 319 | . 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
3 | sylnbi.2 | . 2 ⊢ (¬ 𝜓 → 𝜒) | |
4 | 2, 3 | sylbi 216 | 1 ⊢ (¬ 𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: sylnbir 330 reuun2 4317 opswap 6240 iotanul 6532 riotaund 7420 ndmovcom 7613 suppssov1 8212 suppssov2 8213 suppssfv 8217 brtpos 8250 snnen2oOLD 9261 ranklim 9887 rankuni 9906 ituniiun 10465 hashprb 14414 1mavmul 22541 nonbooli 31584 disjunsn 32514 bj-rest10b 36796 disjrnmpt2 44795 ndmaovcl 46816 ndmaovcom 46818 lindslinindsimp1 47840 setrec2lem1 48439 |
Copyright terms: Public domain | W3C validator |