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  2467  tz6.12-2  6869  fvmptex  7005  f0cli  7094  1st2val  8013  2nd2val  8014  mpoxopxprcov0  8212  rankvaln  9770  alephcard  10053  alephnbtwn  10054  cfub  10231  cardcf  10234  cflecard  10235  cfle  10236  cflim2  10246  cfidm  10258  itunitc1  10403  ituniiun  10405  domtriom  10426  alephreg  10566  pwcfsdom  10567  cfpwsdom  10568  adderpq  10940  mulerpq  10941  sumz  15772  sumss  15774  prod1  15997  prodss  16000  newval  27993  leftval  28007  rightval  28008  lltr  28020  madess  28024  oldssmade  28025  oldss  28028  lrold  28055  r1wf  35431  fpwfvss  44029  grur1cld  44847  afvres  47797  afvco2  47801  ndmaovcl  47828  initopropdlemlem  49901  initopropd  49905  termopropd  49906  zeroopropd  49907