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  4288  opswap  6202  iotanul  6489  riotaund  7383  ndmovcom  7576  suppssov1  8176  suppssov2  8177  suppssfv  8181  brtpos  8214  ranklim  9797  rankuni  9816  ituniiun  10375  hashprb  14362  1mavmul  22435  nonbooli  31580  disjunsn  32523  onvf1odlem4  35093  bj-rest10b  37077  disjrnmpt2  45182  ndmaovcl  47204  ndmaovcom  47206  lindslinindsimp1  48446  lmdfval  49638  cmdfval  49639  setrec2lem1  49682