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  6225  iotanul  6513  riotaund  7409  ndmovcom  7601  suppssov1  8195  suppssov2  8196  suppssfv  8200  brtpos  8233  ranklim  9826  rankuni  9845  ituniiun  10424  hashprb  14461  1mavmul  22770  nonbooli  32132  disjunsn  33067  onvf1odlem4  35703  bj-rest10b  37839  disjrnmpt2  46020  ndmaovcl  48091  ndmaovcom  48093  lindslinindsimp1  49387  lmdfval  50575  cmdfval  50576  setrec2lem1  50619