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  2433  tz6.12-2  6827  fvmptex  6962  f0cli  7050  1st2val  7970  2nd2val  7971  mpoxopxprcov0  8167  rankvaln  9723  alephcard  9992  alephnbtwn  9993  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cfidm  10197  itunitc1  10342  ituniiun  10344  domtriom  10365  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  adderpq  10879  mulerpq  10880  sumz  15684  sumss  15686  prod1  15909  prodss  15912  newval  27827  leftval  27841  rightval  27842  lltr  27854  madess  27858  oldssmade  27859  oldss  27862  lrold  27889  r1wf  35239  fpwfvss  43839  grur1cld  44659  afvres  47620  afvco2  47624  ndmaovcl  47651  initopropdlemlem  49714  initopropd  49718  termopropd  49719  zeroopropd  49720