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  2432  fvmptex  7030  f0cli  7118  1st2val  8041  2nd2val  8042  mpoxopxprcov0  8241  rankvaln  9837  alephcard  10108  alephnbtwn  10109  cfub  10287  cardcf  10290  cflecard  10291  cfle  10292  cflim2  10301  cfidm  10313  itunitc1  10458  ituniiun  10460  domtriom  10481  alephreg  10620  pwcfsdom  10621  cfpwsdom  10622  adderpq  10994  mulerpq  10995  sumz  15755  sumss  15757  prod1  15977  prodss  15980  newval  27909  leftval  27917  rightval  27918  lltropt  27926  madess  27930  oldssmade  27931  lrold  27950  fpwfvss  43402  grur1cld  44228  afvres  47122  afvco2  47126  ndmaovcl  47153