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 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  331  reuun2  4254  opswap  6147  iotanul  6436  riotaund  7304  ndmovcom  7491  suppssov1  8045  suppssfv  8049  brtpos  8082  snnen2oOLD  9048  ranklim  9650  rankuni  9669  ituniiun  10228  hashprb  14161  1mavmul  21746  nonbooli  30062  disjunsn  30982  bj-rest10b  35308  disjrnmpt2  42946  ndmaovcl  44939  ndmaovcom  44941  lindslinindsimp1  46042  setrec2lem1  46643