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  fvmptex  7029  f0cli  7117  1st2val  8043  2nd2val  8044  mpoxopxprcov0  8243  rankvaln  9840  alephcard  10111  alephnbtwn  10112  cfub  10290  cardcf  10293  cflecard  10294  cfle  10295  cflim2  10304  cfidm  10316  itunitc1  10461  ituniiun  10463  domtriom  10484  alephreg  10623  pwcfsdom  10624  cfpwsdom  10625  adderpq  10997  mulerpq  10998  sumz  15759  sumss  15761  prod1  15981  prodss  15984  newval  27895  leftval  27903  rightval  27904  lltropt  27912  madess  27916  oldssmade  27917  lrold  27936  fpwfvss  43430  grur1cld  44256  afvres  47189  afvco2  47193  ndmaovcl  47220