Theorem sylnbi 319

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

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

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 196

This theorem is referenced by:  sylnbir  320  reuun2  3869  opswap  5540  iotanul  5783  riotaund  6546  ndmovcom  6719  suppssov1  7214  suppssfv  7218  brtpos  7248  snnen2o  8034  ranklim  8590  rankuni  8609  cdacomen  8886  ituniiun  9127  hashprb  13046  1mavmul  20173  frgrancvvdeqlem2  26558  frgrawopreglem3  26573  nonbooli  27894  disjunsn  28789  bj-rest10b  32223  ndmaovcl  39932  ndmaovcom  39934  frgrncvvdeqlem2  41470  frgrwopreglem3  41483  lindslinindsimp1  42040