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

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

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 210

This theorem is referenced by:  sylnbir  334  reuun2  4286  opswap  6227  iotanul  6513  riotaund  7404  ndmovcom  7595  suppssov1  8189  suppssov2  8190  suppssfv  8194  brtpos  8227  ranklim  9812  rankuni  9831  ituniiun  10402  hashprb  14429  1mavmul  22670  nonbooli  31940  disjunsn  32876  onvf1odlem4  35485  bj-rest10b  37614  disjrnmpt2  45791  ndmaovcl  47822  ndmaovcom  47824  lindslinindsimp1  49115  lmdfval  50305  cmdfval  50306  setrec2lem1  50349