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  4275  opswap  6211  iotanul  6496  riotaund  7387  ndmovcom  7578  suppssov1  8171  suppssov2  8172  suppssfv  8176  brtpos  8209  ranklim  9796  rankuni  9815  ituniiun  10373  hashprb  14404  1mavmul  22596  nonbooli  31811  disjunsn  32754  onvf1odlem4  35410  bj-rest10b  37540  disjrnmpt2  45727  ndmaovcl  47758  ndmaovcom  47760  lindslinindsimp1  49040  lmdfval  50231  cmdfval  50232  setrec2lem1  50275