Theorem sylnbir 334

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 227	. 2 ⊢ (𝜑 ↔ 𝜓)
3		sylnbir.2	. 2 ⊢ (¬ 𝜓 → 𝜒)
4	2, 3	sylnbi 333	1 ⊢ (¬ 𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  naecoms  2461  tz6.12-2  6868  fvmptex  7004  f0cli  7093  1st2val  8010  2nd2val  8011  mpoxopxprcov0  8209  rankvaln  9767  alephcard  10050  alephnbtwn  10051  cfub  10227  cardcf  10230  cflecard  10231  cfle  10232  cflim2  10242  cfidm  10254  itunitc1  10399  ituniiun  10401  domtriom  10422  alephreg  10562  pwcfsdom  10563  cfpwsdom  10564  adderpq  10936  mulerpq  10937  sumz  15769  sumss  15771  prod1  15994  prodss  15997  newval  28028  leftval  28042  rightval  28043  lltr  28055  madess  28059  oldssmade  28060  oldss  28063  lrold  28090  r1wf  35489  fpwfvss  44138  grur1cld  44956  afvres  47909  afvco2  47913  ndmaovcl  47940  initopropdlemlem  50017  initopropd  50021  termopropd  50022  zeroopropd  50023