Theorem sylnbir 331

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnbir.1	⊢ (𝜓 ↔ 𝜑)
sylnbir.2	⊢ (¬ 𝜓 → 𝜒)

Assertion

Ref	Expression
sylnbir	⊢ (¬ 𝜑 → 𝜒)

Proof of Theorem sylnbir

Step	Hyp	Ref	Expression
1		sylnbir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 224	. 2 ⊢ (𝜑 ↔ 𝜓)
3		sylnbir.2	. 2 ⊢ (¬ 𝜓 → 𝜒)
4	2, 3	sylnbi 330	1 ⊢ (¬ 𝜑 → 𝜒)

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  2437  fvmptex  7043  f0cli  7132  1st2val  8058  2nd2val  8059  mpoxopxprcov0  8258  rankvaln  9868  alephcard  10139  alephnbtwn  10140  cfub  10318  cardcf  10321  cflecard  10322  cfle  10323  cflim2  10332  cfidm  10344  itunitc1  10489  ituniiun  10491  domtriom  10512  alephreg  10651  pwcfsdom  10652  cfpwsdom  10653  adderpq  11025  mulerpq  11026  sumz  15770  sumss  15772  prod1  15992  prodss  15995  newval  27912  leftval  27920  rightval  27921  lltropt  27929  madess  27933  oldssmade  27934  lrold  27953  fpwfvss  43374  grur1cld  44201  afvres  47087  afvco2  47091  ndmaovcl  47118