Theorem sylnbir 320

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 213	. 2 ⊢ (𝜑 ↔ 𝜓)
3		sylnbir.2	. 2 ⊢ (¬ 𝜓 → 𝜒)
4	2, 3	sylnbi 319	1 ⊢ (¬ 𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  naecoms  2301  fvmptex  6203  f0cli  6278  1st2val  7085  2nd2val  7086  mpt2xopxprcov0  7230  rankvaln  8545  alephcard  8776  alephnbtwn  8777  cfub  8954  cardcf  8957  cflecard  8958  cfle  8959  cflim2  8968  cfidm  8980  itunitc1  9125  ituniiun  9127  domtriom  9148  alephreg  9283  pwcfsdom  9284  cfpwsdom  9285  adderpq  9657  mulerpq  9658  sumz  14300  sumss  14302  prod1  14513  prodss  14516  eleenn  25576  afvres  39901  afvco2  39905  ndmaovcl  39932