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 216	1 ⊢ (¬ 𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sylnbir  331  reuun2  4315  opswap  6229  iotanul  6522  riotaund  7405  ndmovcom  7594  suppssov1  8183  suppssfv  8187  brtpos  8220  snnen2oOLD  9227  ranklim  9839  rankuni  9858  ituniiun  10417  hashprb  14357  1mavmul  22050  nonbooli  30935  disjunsn  31856  bj-rest10b  36018  disjrnmpt2  43934  ndmaovcl  45959  ndmaovcom  45961  lindslinindsimp1  47186  setrec2lem1  47786