Theorem sylnbir 334

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  naecoms  2463  tz6.12-2  6872  fvmptex  7008  f0cli  7097  1st2val  8020  2nd2val  8021  mpoxopxprcov0  8219  rankvaln  9778  alephcard  10070  alephnbtwn  10071  cfub  10247  cardcf  10250  cflecard  10251  cfle  10252  cflim2  10262  cfidm  10274  itunitc1  10419  ituniiun  10421  domtriom  10442  alephreg  10582  pwcfsdom  10583  cfpwsdom  10584  adderpq  10956  mulerpq  10957  sumz  15796  sumss  15798  prod1  16021  prodss  16024  newval  28079  leftval  28093  rightval  28094  lltr  28106  madess  28110  oldssmade  28111  oldss  28114  lrold  28141  r1wf  35547  fpwfvss  44196  grur1cld  45014  afvres  47967  afvco2  47971  ndmaovcl  47998  initopropdlemlem  50074  initopropd  50078  termopropd  50079  zeroopropd  50080