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  4270  opswap  6230  iotanul  6518  riotaund  7417  ndmovcom  7609  suppssov1  8218  suppssov2  8219  suppssfv  8223  brtpos  8256  ranklim  9862  rankuni  9883  setrec2lem1  9978  ituniiun  10504  hashprb  14545  1mavmul  22869  nonbooli  32259  disjunsn  33236  onvf1odlem4  35954  bj-rest10b  38103  disjrnmpt2  46297  ndmaovcl  48367  ndmaovcom  48369  lindslinindsimp1  49663  lmdfval  50926  cmdfval  50927