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  2434  tz6.12-2  6829  fvmptex  6964  f0cli  7052  1st2val  7971  2nd2val  7972  mpoxopxprcov0  8169  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  15657  sumss  15659  prod1  15879  prodss  15882  newval  27843  leftval  27857  rightval  27858  lltr  27870  madess  27874  oldssmade  27875  oldss  27878  lrold  27905  r1wf  35273  fpwfvss  43768  grur1cld  44588  afvres  47532  afvco2  47536  ndmaovcl  47563  initopropdlemlem  49598  initopropd  49602  termopropd  49603  zeroopropd  49604