|   | 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 2433 fvmptex 7029 f0cli 7117 1st2val 8043 2nd2val 8044 mpoxopxprcov0 8243 rankvaln 9840 alephcard 10111 alephnbtwn 10112 cfub 10290 cardcf 10293 cflecard 10294 cfle 10295 cflim2 10304 cfidm 10316 itunitc1 10461 ituniiun 10463 domtriom 10484 alephreg 10623 pwcfsdom 10624 cfpwsdom 10625 adderpq 10997 mulerpq 10998 sumz 15759 sumss 15761 prod1 15981 prodss 15984 newval 27895 leftval 27903 rightval 27904 lltropt 27912 madess 27916 oldssmade 27917 lrold 27936 fpwfvss 43430 grur1cld 44256 afvres 47189 afvco2 47193 ndmaovcl 47220 | 
| Copyright terms: Public domain | W3C validator |