Theorem sylnib 677

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 673	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  678  neqcomd  2201  inssdif0im  3518  undifexmid  4226  ordtriexmidlem2  4556  dmsn0el  5139  fidifsnen  6931  ctssdccl  7177  nninfwlpoimlemginf  7242  onntri35  7304  onntri45  7308  2omotaplemap  7324  exmidapne  7327  ltpopr  7662  caucvgprprlemnbj  7760  xrlttri3  9872  fzneuz  10176  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  exp3val  10633  pwle2  15643