Theorem sylnbir 330

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 329	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  6871  f0cli  6956  1st2val  7832  2nd2val  7833  mpoxopxprcov0  8004  rankvaln  9488  alephcard  9757  alephnbtwn  9758  cfub  9936  cardcf  9939  cflecard  9940  cfle  9941  cflim2  9950  cfidm  9962  itunitc1  10107  ituniiun  10109  domtriom  10130  alephreg  10269  pwcfsdom  10270  cfpwsdom  10271  adderpq  10643  mulerpq  10644  sumz  15362  sumss  15364  prod1  15582  prodss  15585  newval  33966  leftval  33974  rightval  33975  madess  33986  oldssmade  33987  lrold  34004  sn-00id  40305  grur1cld  41739  afvres  44551  afvco2  44555  ndmaovcl  44582