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  fvmptex  7030  f0cli  7118  1st2val  8042  2nd2val  8043  mpoxopxprcov0  8242  rankvaln  9839  alephcard  10110  alephnbtwn  10111  cfub  10289  cardcf  10292  cflecard  10293  cfle  10294  cflim2  10303  cfidm  10315  itunitc1  10460  ituniiun  10462  domtriom  10483  alephreg  10622  pwcfsdom  10623  cfpwsdom  10624  adderpq  10996  mulerpq  10997  sumz  15758  sumss  15760  prod1  15980  prodss  15983  newval  27894  leftval  27902  rightval  27903  lltropt  27911  madess  27915  oldssmade  27916  lrold  27935  fpwfvss  43425  grur1cld  44251  afvres  47184  afvco2  47188  ndmaovcl  47215