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  2434  tz6.12-2  6829  fvmptex  6964  f0cli  7052  1st2val  7972  2nd2val  7973  mpoxopxprcov0  8169  rankvaln  9725  alephcard  9994  alephnbtwn  9995  cfub  10173  cardcf  10176  cflecard  10177  cfle  10178  cflim2  10187  cfidm  10199  itunitc1  10344  ituniiun  10346  domtriom  10367  alephreg  10507  pwcfsdom  10508  cfpwsdom  10509  adderpq  10881  mulerpq  10882  sumz  15686  sumss  15688  prod1  15911  prodss  15914  newval  27829  leftval  27843  rightval  27844  lltr  27856  madess  27860  oldssmade  27861  oldss  27864  lrold  27891  r1wf  35241  fpwfvss  43841  grur1cld  44661  afvres  47622  afvco2  47626  ndmaovcl  47653  initopropdlemlem  49716  initopropd  49720  termopropd  49721  zeroopropd  49722