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  4284  opswap  6190  iotanul  6477  riotaund  7365  ndmovcom  7556  suppssov1  8153  suppssov2  8154  suppssfv  8158  brtpos  8191  ranklim  9773  rankuni  9792  ituniiun  10351  hashprb  14338  1mavmul  22411  nonbooli  31553  disjunsn  32496  onvf1odlem4  35066  bj-rest10b  37050  disjrnmpt2  45155  ndmaovcl  47177  ndmaovcom  47179  lindslinindsimp1  48419  lmdfval  49611  cmdfval  49612  setrec2lem1  49655