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  7013  f0cli  7100  1st2val  8003  2nd2val  8004  mpoxopxprcov0  8202  rankvaln  9794  alephcard  10065  alephnbtwn  10066  cfub  10244  cardcf  10247  cflecard  10248  cfle  10249  cflim2  10258  cfidm  10270  itunitc1  10415  ituniiun  10417  domtriom  10438  alephreg  10577  pwcfsdom  10578  cfpwsdom  10579  adderpq  10951  mulerpq  10952  sumz  15668  sumss  15670  prod1  15888  prodss  15891  newval  27351  leftval  27359  rightval  27360  lltropt  27368  madess  27372  oldssmade  27373  lrold  27392  fpwfvss  42211  grur1cld  43039  afvres  45928  afvco2  45932  ndmaovcl  45959