Theorem sylnbi 332

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

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

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 209

This theorem is referenced by:  sylnbir  333  reuun2  4288  opswap  6088  iotanul  6335  riotaund  7155  ndmovcom  7337  suppssov1  7864  suppssfv  7868  brtpos  7903  snnen2o  8709  ranklim  9275  rankuni  9294  ituniiun  9846  hashprb  13761  1mavmul  21159  nonbooli  29430  disjunsn  30346  bj-rest10b  34382  disjrnmpt2  41456  ndmaovcl  43409  ndmaovcom  43411  lindslinindsimp1  44519