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  4279  opswap  6232  iotanul  6518  riotaund  7408  ndmovcom  7599  suppssov1  8194  suppssov2  8195  suppssfv  8199  brtpos  8232  ranklim  9817  rankuni  9836  ituniiun  10407  hashprb  14435  1mavmul  22686  nonbooli  31984  disjunsn  32920  onvf1odlem4  35571  bj-rest10b  37712  disjrnmpt2  45889  ndmaovcl  47923  ndmaovcom  47925  lindslinindsimp1  49220  lmdfval  50410  cmdfval  50411  setrec2lem1  50454