Theorem sylnbi 331

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnbi.1	⊢ (𝜑 ↔ 𝜓)
sylnbi.2	⊢ (¬ 𝜓 → 𝜒)

Assertion

Ref	Expression
sylnbi	⊢ (¬ 𝜑 → 𝜒)

Proof of Theorem sylnbi

Step	Hyp	Ref	Expression
1		sylnbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	notbii 321	. 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
3		sylnbi.2	. 2 ⊢ (¬ 𝜓 → 𝜒)
4	2, 3	sylbi 218	1 ⊢ (¬ 𝜑 → 𝜒)

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

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 208

This theorem is referenced by:  sylnbir  332  reuun2  4253  opswap  6180  iotanul  6465  riotaund  7352  ndmovcom  7543  suppssov1  8137  suppssov2  8138  suppssfv  8142  brtpos  8175  ranklim  9759  rankuni  9778  ituniiun  10335  hashprb  14350  1mavmul  22531  nonbooli  31740  disjunsn  32683  onvf1odlem4  35334  bj-rest10b  37447  disjrnmpt2  45635  ndmaovcl  47666  ndmaovcom  47668  lindslinindsimp1  48948  lmdfval  50139  cmdfval  50140  setrec2lem1  50183