![]() |
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 4274 opswap 6181 iotanul 6474 riotaund 7353 ndmovcom 7541 suppssov1 8129 suppssfv 8133 brtpos 8166 snnen2oOLD 9171 ranklim 9780 rankuni 9799 ituniiun 10358 hashprb 14297 1mavmul 21897 nonbooli 30593 disjunsn 31512 bj-rest10b 35560 disjrnmpt2 43397 ndmaovcl 45425 ndmaovcom 45427 lindslinindsimp1 46528 setrec2lem1 47128 |
Copyright terms: Public domain | W3C validator |