Theorem sylnib 687

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnib.1	⊢ (𝜑 → ¬ 𝜓)
sylnib.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
sylnib	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem sylnib

Step	Hyp	Ref	Expression
1		sylnib.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		sylnib.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	a1i 9	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	1, 3	mtbid 683	1 ⊢ (𝜑 → ¬ 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  688  neqcomd  2243  inssdif0imOLD  3593  undifexmid  4328  ordtriexmidlem2  4665  dmsn0el  5255  fidifsnen  7166  ctssdccl  7445  nninfwlpoimlemginf  7510  onntri35  7590  onntri45  7594  2omotaplemap  7617  exmidapne  7620  ltpopr  7956  caucvgprprlemnbj  8054  xrlttri3  10182  fzneuz  10491  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemab  10922  exp3val  10961  ballotfilemimin  13232  ballotfilemfrcn0  13256  pwle2  17011