Theorem sylnbir 330

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 329	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  2428  fvmptex  7009  f0cli  7096  1st2val  7999  2nd2val  8000  mpoxopxprcov0  8198  rankvaln  9790  alephcard  10061  alephnbtwn  10062  cfub  10240  cardcf  10243  cflecard  10244  cfle  10245  cflim2  10254  cfidm  10266  itunitc1  10411  ituniiun  10413  domtriom  10434  alephreg  10573  pwcfsdom  10574  cfpwsdom  10575  adderpq  10947  mulerpq  10948  sumz  15664  sumss  15666  prod1  15884  prodss  15887  newval  27339  leftval  27347  rightval  27348  lltropt  27356  madess  27360  oldssmade  27361  lrold  27380  fpwfvss  42148  grur1cld  42976  afvres  45866  afvco2  45870  ndmaovcl  45897