Theorem sylnbi 330

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 320	. 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
3		sylnbi.2	. 2 ⊢ (¬ 𝜓 → 𝜒)
4	2, 3	sylbi 217	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:  sylnbir  331  reuun2  4265  opswap  6193  iotanul  6478  riotaund  7363  ndmovcom  7554  suppssov1  8147  suppssov2  8148  suppssfv  8152  brtpos  8185  ranklim  9768  rankuni  9787  ituniiun  10344  hashprb  14359  1mavmul  22513  nonbooli  31722  disjunsn  32664  onvf1odlem4  35288  bj-rest10b  37401  disjrnmpt2  45618  ndmaovcl  47651  ndmaovcom  47653  lindslinindsimp1  48933  lmdfval  50124  cmdfval  50125  setrec2lem1  50168