|   | 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 224 | . 2 ⊢ (𝜑 ↔ 𝜓) | 
| 3 | sylnbir.2 | . 2 ⊢ (¬ 𝜓 → 𝜒) | |
| 4 | 2, 3 | sylnbi 330 | 1 ⊢ (¬ 𝜑 → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 | 
| 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 207 | 
| This theorem is referenced by: naecoms 2434 fvmptex 7030 f0cli 7118 1st2val 8042 2nd2val 8043 mpoxopxprcov0 8242 rankvaln 9839 alephcard 10110 alephnbtwn 10111 cfub 10289 cardcf 10292 cflecard 10293 cfle 10294 cflim2 10303 cfidm 10315 itunitc1 10460 ituniiun 10462 domtriom 10483 alephreg 10622 pwcfsdom 10623 cfpwsdom 10624 adderpq 10996 mulerpq 10997 sumz 15758 sumss 15760 prod1 15980 prodss 15983 newval 27894 leftval 27902 rightval 27903 lltropt 27911 madess 27915 oldssmade 27916 lrold 27935 fpwfvss 43425 grur1cld 44251 afvres 47184 afvco2 47188 ndmaovcl 47215 | 
| Copyright terms: Public domain | W3C validator |