Theorem sylnbir 332

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

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

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 208

This theorem is referenced by:  naecoms  2437  tz6.12-2  6814  fvmptex  6950  f0cli  7039  1st2val  7959  2nd2val  7960  mpoxopxprcov0  8157  rankvaln  9714  alephcard  9983  alephnbtwn  9984  cfub  10162  cardcf  10165  cflecard  10166  cfle  10167  cflim2  10176  cfidm  10188  itunitc1  10333  ituniiun  10335  domtriom  10356  alephreg  10496  pwcfsdom  10497  cfpwsdom  10498  adderpq  10870  mulerpq  10871  sumz  15675  sumss  15677  prod1  15900  prodss  15903  newval  27845  leftval  27859  rightval  27860  lltr  27872  madess  27876  oldssmade  27877  oldss  27880  lrold  27907  r1wf  35277  fpwfvss  43856  grur1cld  44676  afvres  47635  afvco2  47639  ndmaovcl  47666  initopropdlemlem  49729  initopropd  49733  termopropd  49734  zeroopropd  49735