Theorem sylnbi 322

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

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

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 199

This theorem is referenced by:  sylnbir  323  reuun2  4136  opswap  5876  iotanul  6114  riotaund  6919  ndmovcom  7098  suppssov1  7609  suppssfv  7613  brtpos  7643  snnen2o  8437  ranklim  9004  rankuni  9023  cdacomen  9338  ituniiun  9579  hashprb  13499  1mavmul  20759  nonbooli  29082  disjunsn  29970  bj-rest10b  33615  ndmaovcl  42244  ndmaovcom  42246  lindslinindsimp1  43261