Theorem sylnbi 330

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

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

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 207

This theorem is referenced by:  sylnbir  331  reuun2  4266  opswap  6187  iotanul  6472  riotaund  7356  ndmovcom  7547  suppssov1  8140  suppssov2  8141  suppssfv  8145  brtpos  8178  ranklim  9759  rankuni  9778  ituniiun  10335  hashprb  14350  1mavmul  22523  nonbooli  31737  disjunsn  32679  onvf1odlem4  35304  bj-rest10b  37417  disjrnmpt2  45636  ndmaovcl  47663  ndmaovcom  47665  lindslinindsimp1  48945  lmdfval  50136  cmdfval  50137  setrec2lem1  50180