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  2429  tz6.12-2  6809  fvmptex  6943  f0cli  7031  1st2val  7949  2nd2val  7950  mpoxopxprcov0  8147  rankvaln  9692  alephcard  9961  alephnbtwn  9962  cfub  10140  cardcf  10143  cflecard  10144  cfle  10145  cflim2  10154  cfidm  10166  itunitc1  10311  ituniiun  10313  domtriom  10334  alephreg  10473  pwcfsdom  10474  cfpwsdom  10475  adderpq  10847  mulerpq  10848  sumz  15629  sumss  15631  prod1  15851  prodss  15854  newval  27796  leftval  27804  rightval  27805  lltropt  27817  madess  27821  oldssmade  27822  oldss  27823  lrold  27842  r1wf  35107  fpwfvss  43453  grur1cld  44273  afvres  47211  afvco2  47215  ndmaovcl  47242  initopropdlemlem  49279  initopropd  49283  termopropd  49284  zeroopropd  49285