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  2428  fvmptex  6985  f0cli  7073  1st2val  7999  2nd2val  8000  mpoxopxprcov0  8199  rankvaln  9759  alephcard  10030  alephnbtwn  10031  cfub  10209  cardcf  10212  cflecard  10213  cfle  10214  cflim2  10223  cfidm  10235  itunitc1  10380  ituniiun  10382  domtriom  10403  alephreg  10542  pwcfsdom  10543  cfpwsdom  10544  adderpq  10916  mulerpq  10917  sumz  15695  sumss  15697  prod1  15917  prodss  15920  newval  27770  leftval  27778  rightval  27779  lltropt  27791  madess  27795  oldssmade  27796  lrold  27815  fpwfvss  43408  grur1cld  44228  afvres  47177  afvco2  47181  ndmaovcl  47208  initopropdlemlem  49232  initopropd  49236  termopropd  49237  zeroopropd  49238