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

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

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 197

This theorem is referenced by:  naecoms  2346  fvmptex  6333  f0cli  6410  1st2val  7238  2nd2val  7239  mpt2xopxprcov0  7388  rankvaln  8700  alephcard  8931  alephnbtwn  8932  cfub  9109  cardcf  9112  cflecard  9113  cfle  9114  cflim2  9123  cfidm  9135  itunitc1  9280  ituniiun  9282  domtriom  9303  alephreg  9442  pwcfsdom  9443  cfpwsdom  9444  adderpq  9816  mulerpq  9817  sumz  14497  sumss  14499  prod1  14718  prodss  14721  eleenn  25821  afvres  41573  afvco2  41577  ndmaovcl  41604