Theorem sylnbir 333

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

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

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 209

This theorem is referenced by:  naecoms  2451  fvmptex  6784  f0cli  6866  1st2val  7719  2nd2val  7720  mpoxopxprcov0  7885  rankvaln  9230  alephcard  9498  alephnbtwn  9499  cfub  9673  cardcf  9676  cflecard  9677  cfle  9678  cflim2  9687  cfidm  9699  itunitc1  9844  ituniiun  9846  domtriom  9867  alephreg  10006  pwcfsdom  10007  cfpwsdom  10008  adderpq  10380  mulerpq  10381  sumz  15081  sumss  15083  prod1  15300  prodss  15303  sn-00id  39238  grur1cld  40575  afvres  43378  afvco2  43382  ndmaovcl  43409