Theorem sylnbir 331

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  naecoms  2433  tz6.12-2  6821  fvmptex  6955  f0cli  7043  1st2val  7961  2nd2val  7962  mpoxopxprcov0  8159  rankvaln  9711  alephcard  9980  alephnbtwn  9981  cfub  10159  cardcf  10162  cflecard  10163  cfle  10164  cflim2  10173  cfidm  10185  itunitc1  10330  ituniiun  10332  domtriom  10353  alephreg  10493  pwcfsdom  10494  cfpwsdom  10495  adderpq  10867  mulerpq  10868  sumz  15645  sumss  15647  prod1  15867  prodss  15870  newval  27831  leftval  27845  rightval  27846  lltr  27858  madess  27862  oldssmade  27863  oldss  27866  lrold  27893  r1wf  35252  fpwfvss  43653  grur1cld  44473  afvres  47418  afvco2  47422  ndmaovcl  47449  initopropdlemlem  49484  initopropd  49488  termopropd  49489  zeroopropd  49490