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  4273  opswap  6249  iotanul  6545  riotaund  7447  ndmovcom  7640  suppssov1  8252  suppssov2  8253  suppssfv  8257  brtpos  8290  ranklim  9895  rankuni  9916  setrec2lem1  10011  ituniiun  10539  hashprb  14582  1mavmul  22918  nonbooli  32310  disjunsn  33286  onvf1odlem4  36075  bj-rest10b  38280  disjrnmpt2  46476  ndmaovcl  48546  ndmaovcom  48548  lindslinindsimp1  49900  lmdfval  51163  cmdfval  51164