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  4253  opswap  6129  iotanul  6408  riotaund  7265  ndmovcom  7450  suppssov1  7998  suppssfv  8002  brtpos  8035  snnen2o  8963  ranklim  9586  rankuni  9605  ituniiun  10162  hashprb  14093  1mavmul  21678  nonbooli  29992  disjunsn  30912  bj-rest10b  35239  disjrnmpt2  42679  ndmaovcl  44646  ndmaovcom  44648  lindslinindsimp1  45750  setrec2lem1  46351