Theorem sylnbir 323

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

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

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 199

This theorem is referenced by:  naecoms  2395  fvmptex  6557  f0cli  6636  1st2val  7475  2nd2val  7476  mpt2xopxprcov0  7627  rankvaln  8961  alephcard  9228  alephnbtwn  9229  cfub  9408  cardcf  9411  cflecard  9412  cfle  9413  cflim2  9422  cfidm  9434  itunitc1  9579  ituniiun  9581  domtriom  9602  alephreg  9741  pwcfsdom  9742  cfpwsdom  9743  adderpq  10115  mulerpq  10116  sumz  14864  sumss  14866  prod1  15081  prodss  15084  eleenn  26249  afvres  42223  afvco2  42227  ndmaovcl  42254