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

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

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 206

This theorem is referenced by:  naecoms  2429  fvmptex  7010  f0cli  7097  1st2val  8000  2nd2val  8001  mpoxopxprcov0  8199  rankvaln  9791  alephcard  10062  alephnbtwn  10063  cfub  10241  cardcf  10244  cflecard  10245  cfle  10246  cflim2  10255  cfidm  10267  itunitc1  10412  ituniiun  10414  domtriom  10435  alephreg  10574  pwcfsdom  10575  cfpwsdom  10576  adderpq  10948  mulerpq  10949  sumz  15665  sumss  15667  prod1  15885  prodss  15888  newval  27340  leftval  27348  rightval  27349  lltropt  27357  madess  27361  oldssmade  27362  lrold  27381  fpwfvss  42149  grur1cld  42977  afvres  45867  afvco2  45871  ndmaovcl  45898