Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sylnbir | Structured version Visualization version GIF version |
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnbir.1 | ⊢ (𝜓 ↔ 𝜑) |
sylnbir.2 | ⊢ (¬ 𝜓 → 𝜒) |
Ref | Expression |
---|---|
sylnbir | ⊢ (¬ 𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnbir.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | bicomi 213 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | sylnbir.2 | . 2 ⊢ (¬ 𝜓 → 𝜒) | |
4 | 2, 3 | sylnbi 319 | 1 ⊢ (¬ 𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: naecoms 2301 fvmptex 6203 f0cli 6278 1st2val 7085 2nd2val 7086 mpt2xopxprcov0 7230 rankvaln 8545 alephcard 8776 alephnbtwn 8777 cfub 8954 cardcf 8957 cflecard 8958 cfle 8959 cflim2 8968 cfidm 8980 itunitc1 9125 ituniiun 9127 domtriom 9148 alephreg 9283 pwcfsdom 9284 cfpwsdom 9285 adderpq 9657 mulerpq 9658 sumz 14300 sumss 14302 prod1 14513 prodss 14516 eleenn 25576 afvres 39901 afvco2 39905 ndmaovcl 39932 |
Copyright terms: Public domain | W3C validator |