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  6865  fvmptex  7001  f0cli  7091  1st2val  8014  2nd2val  8015  mpoxopxprcov0  8215  rankvaln  9781  alephcard  10073  alephnbtwn  10074  cfub  10250  cardcf  10253  cflecard  10254  cfle  10255  cflim2  10265  cfidm  10277  itunitc1  10422  ituniiun  10424  domtriom  10445  alephreg  10591  pwcfsdom  10592  cfpwsdom  10593  adderpq  10965  mulerpq  10966  sumz  15808  sumss  15810  prod1  16031  prodss  16034  newval  28100  leftval  28114  rightval  28115  lltr  28127  madess  28131  oldssmade  28132  oldss  28135  lrold  28162  r1wf  35603  fpwfvss  44252  grur1cld  45070  afvres  48060  afvco2  48064  ndmaovcl  48091  initopropdlemlem  50165  initopropd  50169  termopropd  50170  zeroopropd  50171