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  4274  opswap  6184  iotanul  6469  riotaund  7351  ndmovcom  7542  suppssov1  8136  suppssov2  8137  suppssfv  8141  brtpos  8174  ranklim  9748  rankuni  9767  ituniiun  10324  hashprb  14311  1mavmul  22483  nonbooli  31652  disjunsn  32595  onvf1odlem4  35222  bj-rest10b  37206  disjrnmpt2  45348  ndmaovcl  47365  ndmaovcom  47367  lindslinindsimp1  48619  lmdfval  49810  cmdfval  49811  setrec2lem1  49854