Theorem sylnbir 333

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

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

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 209

This theorem is referenced by:  naecoms  2460  tz6.12-2  6854  fvmptex  6990  f0cli  7079  1st2val  7998  2nd2val  7999  mpoxopxprcov0  8197  rankvaln  9757  alephcard  10026  alephnbtwn  10027  cfub  10205  cardcf  10208  cflecard  10209  cfle  10210  cflim2  10220  cfidm  10232  itunitc1  10377  ituniiun  10379  domtriom  10400  alephreg  10540  pwcfsdom  10541  cfpwsdom  10542  adderpq  10914  mulerpq  10915  sumz  15749  sumss  15751  prod1  15974  prodss  15977  newval  27925  leftval  27939  rightval  27940  lltr  27952  madess  27956  oldssmade  27957  oldss  27960  lrold  27987  r1wf  35389  fpwfvss  43985  grur1cld  44805  afvres  47763  afvco2  47767  ndmaovcl  47794  initopropdlemlem  49857  initopropd  49861  termopropd  49862  zeroopropd  49863