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  2427  fvmptex  6964  f0cli  7052  1st2val  7975  2nd2val  7976  mpoxopxprcov0  8173  rankvaln  9728  alephcard  9999  alephnbtwn  10000  cfub  10178  cardcf  10181  cflecard  10182  cfle  10183  cflim2  10192  cfidm  10204  itunitc1  10349  ituniiun  10351  domtriom  10372  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  adderpq  10885  mulerpq  10886  sumz  15664  sumss  15666  prod1  15886  prodss  15889  newval  27739  leftval  27747  rightval  27748  lltropt  27760  madess  27764  oldssmade  27765  lrold  27784  fpwfvss  43374  grur1cld  44194  afvres  47146  afvco2  47150  ndmaovcl  47177  initopropdlemlem  49201  initopropd  49205  termopropd  49206  zeroopropd  49207