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  2431  tz6.12-2  6819  fvmptex  6953  f0cli  7041  1st2val  7959  2nd2val  7960  mpoxopxprcov0  8157  rankvaln  9709  alephcard  9978  alephnbtwn  9979  cfub  10157  cardcf  10160  cflecard  10161  cfle  10162  cflim2  10171  cfidm  10183  itunitc1  10328  ituniiun  10330  domtriom  10351  alephreg  10491  pwcfsdom  10492  cfpwsdom  10493  adderpq  10865  mulerpq  10866  sumz  15643  sumss  15645  prod1  15865  prodss  15868  newval  27823  leftval  27831  rightval  27832  lltropt  27844  madess  27848  oldssmade  27849  oldss  27850  lrold  27869  r1wf  35201  fpwfvss  43595  grur1cld  44415  afvres  47360  afvco2  47364  ndmaovcl  47391  initopropdlemlem  49426  initopropd  49430  termopropd  49431  zeroopropd  49432