Theorem sylnbi 333

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 323	. 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
3		sylnbi.2	. 2 ⊢ (¬ 𝜓 → 𝜒)
4	2, 3	sylbi 220	1 ⊢ (¬ 𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sylnbir  334  reuun2  4271  opswap  6229  iotanul  6517  riotaund  7414  ndmovcom  7606  suppssov1  8207  suppssov2  8208  suppssfv  8212  brtpos  8245  ranklim  9851  rankuni  9872  setrec2lem1  9967  ituniiun  10493  hashprb  14534  1mavmul  22856  nonbooli  32246  disjunsn  33181  onvf1odlem4  35868  bj-rest10b  37990  disjrnmpt2  46172  ndmaovcl  48242  ndmaovcom  48244  lindslinindsimp1  49538  lmdfval  50726  cmdfval  50727