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  4279  opswap  6195  iotanul  6480  riotaund  7364  ndmovcom  7555  suppssov1  8149  suppssov2  8150  suppssfv  8154  brtpos  8187  ranklim  9768  rankuni  9787  ituniiun  10344  hashprb  14332  1mavmul  22504  nonbooli  31738  disjunsn  32680  onvf1odlem4  35319  bj-rest10b  37339  disjrnmpt2  45544  ndmaovcl  47560  ndmaovcom  47562  lindslinindsimp1  48814  lmdfval  50005  cmdfval  50006  setrec2lem1  50049