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  2434  fvmptex  7005  f0cli  7093  1st2val  8021  2nd2val  8022  mpoxopxprcov0  8221  rankvaln  9818  alephcard  10089  alephnbtwn  10090  cfub  10268  cardcf  10271  cflecard  10272  cfle  10273  cflim2  10282  cfidm  10294  itunitc1  10439  ituniiun  10441  domtriom  10462  alephreg  10601  pwcfsdom  10602  cfpwsdom  10603  adderpq  10975  mulerpq  10976  sumz  15743  sumss  15745  prod1  15965  prodss  15968  newval  27820  leftval  27828  rightval  27829  lltropt  27841  madess  27845  oldssmade  27846  lrold  27865  fpwfvss  43403  grur1cld  44223  afvres  47168  afvco2  47172  ndmaovcl  47199  initopropdlemlem  49123  initopropd  49127  termopropd  49128  zeroopropd  49129