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  2427  fvmptex  6944  f0cli  7032  1st2val  7952  2nd2val  7953  mpoxopxprcov0  8150  rankvaln  9695  alephcard  9964  alephnbtwn  9965  cfub  10143  cardcf  10146  cflecard  10147  cfle  10148  cflim2  10157  cfidm  10169  itunitc1  10314  ituniiun  10316  domtriom  10337  alephreg  10476  pwcfsdom  10477  cfpwsdom  10478  adderpq  10850  mulerpq  10851  sumz  15629  sumss  15631  prod1  15851  prodss  15854  newval  27765  leftval  27773  rightval  27774  lltropt  27786  madess  27790  oldssmade  27791  oldss  27792  lrold  27811  fpwfvss  43385  grur1cld  44205  afvres  47156  afvco2  47160  ndmaovcl  47187  initopropdlemlem  49224  initopropd  49228  termopropd  49229  zeroopropd  49230