![]() |
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 223 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | sylnbir.2 | . 2 ⊢ (¬ 𝜓 → 𝜒) | |
4 | 2, 3 | sylnbi 330 | 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: naecoms 2429 fvmptex 7010 f0cli 7097 1st2val 8000 2nd2val 8001 mpoxopxprcov0 8199 rankvaln 9791 alephcard 10062 alephnbtwn 10063 cfub 10241 cardcf 10244 cflecard 10245 cfle 10246 cflim2 10255 cfidm 10267 itunitc1 10412 ituniiun 10414 domtriom 10435 alephreg 10574 pwcfsdom 10575 cfpwsdom 10576 adderpq 10948 mulerpq 10949 sumz 15665 sumss 15667 prod1 15885 prodss 15888 newval 27340 leftval 27348 rightval 27349 lltropt 27357 madess 27361 oldssmade 27362 lrold 27381 fpwfvss 42149 grur1cld 42977 afvres 45867 afvco2 45871 ndmaovcl 45898 |
Copyright terms: Public domain | W3C validator |