Theorem sylnbir 331

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

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

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 206

This theorem is referenced by:  naecoms  2429  fvmptex  6889  f0cli  6974  1st2val  7859  2nd2val  7860  mpoxopxprcov0  8033  rankvaln  9557  alephcard  9826  alephnbtwn  9827  cfub  10005  cardcf  10008  cflecard  10009  cfle  10010  cflim2  10019  cfidm  10031  itunitc1  10176  ituniiun  10178  domtriom  10199  alephreg  10338  pwcfsdom  10339  cfpwsdom  10340  adderpq  10712  mulerpq  10713  sumz  15434  sumss  15436  prod1  15654  prodss  15657  newval  34039  leftval  34047  rightval  34048  madess  34059  oldssmade  34060  lrold  34077  sn-00id  40384  grur1cld  41850  afvres  44664  afvco2  44668  ndmaovcl  44695