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  2447  fvmptex  6776  f0cli  6858  1st2val  7711  2nd2val  7712  mpoxopxprcov0  7877  rankvaln  9222  alephcard  9490  alephnbtwn  9491  cfub  9665  cardcf  9668  cflecard  9669  cfle  9670  cflim2  9679  cfidm  9691  itunitc1  9836  ituniiun  9838  domtriom  9859  alephreg  9998  pwcfsdom  9999  cfpwsdom  10000  adderpq  10372  mulerpq  10373  sumz  15073  sumss  15075  prod1  15292  prodss  15295  sn-00id  39224  grur1cld  40561  afvres  43365  afvco2  43369  ndmaovcl  43396