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 ⊢ (¬ 𝜑 → 𝜒)

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

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 210

This theorem is referenced by:  sylnbir  334  reuun2  4215  opswap  6072  iotanul  6336  riotaund  7188  ndmovcom  7373  suppssov1  7918  suppssfv  7922  brtpos  7955  snnen2o  8814  ranklim  9425  rankuni  9444  ituniiun  10001  hashprb  13929  1mavmul  21399  nonbooli  29686  disjunsn  30606  bj-rest10b  34944  disjrnmpt2  42340  ndmaovcl  44310  ndmaovcom  44312  lindslinindsimp1  45414  setrec2lem1  46013