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  2458  tz6.12-2  6877  fvmptex  7013  f0cli  7103  1st2val  8033  2nd2val  8034  mpoxopxprcov0  8241  rankvaln  9814  r1wf  9848  alephcard  10156  alephnbtwn  10157  cfub  10333  cardcf  10336  cflecard  10337  cfle  10338  cflim2  10348  cfidm  10360  itunitc1  10505  ituniiun  10507  domtriom  10528  alephreg  10674  pwcfsdom  10675  cfpwsdom  10676  adderpq  11048  mulerpq  11049  sumz  15897  sumss  15899  prod1  16120  prodss  16123  newval  28230  leftval  28244  rightval  28245  lltr  28257  madess  28261  oldssmade  28262  oldss  28265  lrold  28292  rmo6  35760  acwer1prclem  35819  j0ltaleph  35951  fpwfvss  44522  grur1cld  45339  afvres  48350  afvco2  48354  ndmaovcl  48381  initopropdlemlem  50469  initopropd  50473  termopropd  50474  zeroopropd  50475