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  2461  tz6.12-2  6903  fvmptex  7039  f0cli  7130  1st2val  8063  2nd2val  8064  mpoxopxprcov0  8272  rankvaln  9844  r1wf  9878  alephcard  10188  alephnbtwn  10189  cfub  10365  cardcf  10368  cflecard  10369  cfle  10370  cflim2  10380  cfidm  10392  itunitc1  10537  ituniiun  10539  domtriom  10560  alephreg  10706  pwcfsdom  10707  cfpwsdom  10708  adderpq  11080  mulerpq  11081  sumz  15932  sumss  15934  prod1  16155  prodss  16158  newval  28278  leftval  28292  rightval  28293  lltr  28305  madess  28309  oldssmade  28310  oldss  28313  lrold  28340  rmo6  35821  acwer1prclem  35892  j0ltaleph  36049  jltaleph  36067  fpwfvss  44674  grur1cld  45491  afvres  48515  afvco2  48519  ndmaovcl  48546  initopropdlemlem  50692  initopropd  50696  termopropd  50697  zeroopropd  50698