Theorem sylnbir 334

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

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

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 210

This theorem is referenced by:  naecoms  2428  fvmptex  6810  f0cli  6895  1st2val  7767  2nd2val  7768  mpoxopxprcov0  7937  rankvaln  9380  alephcard  9649  alephnbtwn  9650  cfub  9828  cardcf  9831  cflecard  9832  cfle  9833  cflim2  9842  cfidm  9854  itunitc1  9999  ituniiun  10001  domtriom  10022  alephreg  10161  pwcfsdom  10162  cfpwsdom  10163  adderpq  10535  mulerpq  10536  sumz  15251  sumss  15253  prod1  15469  prodss  15472  newval  33725  leftval  33733  rightval  33734  madess  33745  oldssmade  33746  lrold  33763  sn-00id  40033  grur1cld  41464  afvres  44279  afvco2  44283  ndmaovcl  44310