Theorem sylnbi 329

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 319	. 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  330  reuun2  4317  opswap  6240  iotanul  6532  riotaund  7420  ndmovcom  7613  suppssov1  8212  suppssov2  8213  suppssfv  8217  brtpos  8250  snnen2oOLD  9261  ranklim  9887  rankuni  9906  ituniiun  10465  hashprb  14414  1mavmul  22541  nonbooli  31584  disjunsn  32514  bj-rest10b  36796  disjrnmpt2  44795  ndmaovcl  46816  ndmaovcom  46818  lindslinindsimp1  47840  setrec2lem1  48439