Theorem sylnbi 329

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

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

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 206

This theorem is referenced by:  sylnbir  330  reuun2  4314  opswap  6228  iotanul  6521  riotaund  7404  ndmovcom  7593  suppssov1  8182  suppssfv  8186  brtpos  8219  snnen2oOLD  9226  ranklim  9838  rankuni  9857  ituniiun  10416  hashprb  14356  1mavmul  22049  nonbooli  30899  disjunsn  31820  bj-rest10b  35965  disjrnmpt2  43876  ndmaovcl  45901  ndmaovcom  45903  lindslinindsimp1  47128  setrec2lem1  47728