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  4270  opswap  6171  iotanul  6456  riotaund  7337  ndmovcom  7528  suppssov1  8122  suppssov2  8123  suppssfv  8127  brtpos  8160  ranklim  9732  rankuni  9751  ituniiun  10308  hashprb  14299  1mavmul  22458  nonbooli  31623  disjunsn  32566  onvf1odlem4  35142  bj-rest10b  37123  disjrnmpt2  45225  ndmaovcl  47234  ndmaovcom  47236  lindslinindsimp1  48489  lmdfval  49681  cmdfval  49682  setrec2lem1  49725