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  6822  fvmptex  6957  f0cli  7045  1st2val  7964  2nd2val  7965  mpoxopxprcov0  8161  rankvaln  9717  alephcard  9986  alephnbtwn  9987  cfub  10165  cardcf  10168  cflecard  10169  cfle  10170  cflim2  10179  cfidm  10191  itunitc1  10336  ituniiun  10338  domtriom  10359  alephreg  10499  pwcfsdom  10500  cfpwsdom  10501  adderpq  10873  mulerpq  10874  sumz  15678  sumss  15680  prod1  15903  prodss  15906  newval  27844  leftval  27858  rightval  27859  lltr  27871  madess  27875  oldssmade  27876  oldss  27879  lrold  27906  r1wf  35258  fpwfvss  43860  grur1cld  44680  afvres  47635  afvco2  47639  ndmaovcl  47666  initopropdlemlem  49729  initopropd  49733  termopropd  49734  zeroopropd  49735