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  6982  f0cli  7070  1st2val  7996  2nd2val  7997  mpoxopxprcov0  8196  rankvaln  9752  alephcard  10023  alephnbtwn  10024  cfub  10202  cardcf  10205  cflecard  10206  cfle  10207  cflim2  10216  cfidm  10228  itunitc1  10373  ituniiun  10375  domtriom  10396  alephreg  10535  pwcfsdom  10536  cfpwsdom  10537  adderpq  10909  mulerpq  10910  sumz  15688  sumss  15690  prod1  15910  prodss  15913  newval  27763  leftval  27771  rightval  27772  lltropt  27784  madess  27788  oldssmade  27789  lrold  27808  fpwfvss  43401  grur1cld  44221  afvres  47173  afvco2  47177  ndmaovcl  47204  initopropdlemlem  49228  initopropd  49232  termopropd  49233  zeroopropd  49234