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  2427  fvmptex  6964  f0cli  7052  1st2val  7975  2nd2val  7976  mpoxopxprcov0  8173  rankvaln  9728  alephcard  9999  alephnbtwn  10000  cfub  10178  cardcf  10181  cflecard  10182  cfle  10183  cflim2  10192  cfidm  10204  itunitc1  10349  ituniiun  10351  domtriom  10372  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  adderpq  10885  mulerpq  10886  sumz  15664  sumss  15666  prod1  15886  prodss  15889  newval  27800  leftval  27808  rightval  27809  lltropt  27821  madess  27825  oldssmade  27826  oldss  27827  lrold  27846  fpwfvss  43394  grur1cld  44214  afvres  47166  afvco2  47170  ndmaovcl  47197  initopropdlemlem  49221  initopropd  49225  termopropd  49226  zeroopropd  49227