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  2459  tz6.12-2  6870  fvmptex  7006  f0cli  7096  1st2val  8027  2nd2val  8028  mpoxopxprcov0  8227  rankvaln  9800  r1wf  9834  alephcard  10142  alephnbtwn  10143  cfub  10319  cardcf  10322  cflecard  10323  cfle  10324  cflim2  10334  cfidm  10346  itunitc1  10491  ituniiun  10493  domtriom  10514  alephreg  10660  pwcfsdom  10661  cfpwsdom  10662  adderpq  11034  mulerpq  11035  sumz  15881  sumss  15883  prod1  16104  prodss  16107  newval  28214  leftval  28228  rightval  28229  lltr  28241  madess  28245  oldssmade  28246  oldss  28249  lrold  28276  fpwfvss  44397  grur1cld  45215  afvres  48211  afvco2  48215  ndmaovcl  48242  initopropdlemlem  50316  initopropd  50320  termopropd  50321  zeroopropd  50322