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  4277  opswap  6187  iotanul  6472  riotaund  7354  ndmovcom  7545  suppssov1  8139  suppssov2  8140  suppssfv  8144  brtpos  8177  ranklim  9756  rankuni  9775  ituniiun  10332  hashprb  14320  1mavmul  22492  nonbooli  31726  disjunsn  32669  onvf1odlem4  35300  bj-rest10b  37294  disjrnmpt2  45432  ndmaovcl  47449  ndmaovcom  47451  lindslinindsimp1  48703  lmdfval  49894  cmdfval  49895  setrec2lem1  49938