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  4278  opswap  6182  iotanul  6466  riotaund  7349  ndmovcom  7540  suppssov1  8137  suppssov2  8138  suppssfv  8142  brtpos  8175  ranklim  9759  rankuni  9778  ituniiun  10335  hashprb  14322  1mavmul  22451  nonbooli  31613  disjunsn  32556  onvf1odlem4  35081  bj-rest10b  37065  disjrnmpt2  45169  ndmaovcl  47191  ndmaovcom  47193  lindslinindsimp1  48446  lmdfval  49638  cmdfval  49639  setrec2lem1  49682