Theorem sylnbi 333

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 323	. 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
3		sylnbi.2	. 2 ⊢ (¬ 𝜓 → 𝜒)
4	2, 3	sylbi 220	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:  sylnbir  334  reuun2  4278  opswap  6232  iotanul  6520  riotaund  7412  ndmovcom  7603  suppssov1  8195  suppssov2  8196  suppssfv  8200  brtpos  8233  ranklim  9819  rankuni  9838  ituniiun  10417  hashprb  14447  1mavmul  22735  nonbooli  32050  disjunsn  32986  onvf1odlem4  35623  bj-rest10b  37764  disjrnmpt2  45939  ndmaovcl  47973  ndmaovcom  47975  lindslinindsimp1  49270  lmdfval  50460  cmdfval  50461  setrec2lem1  50504