Theorem sylnib 680

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 676	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  681  neqcomd  2234  inssdif0im  3559  undifexmid  4277  ordtriexmidlem2  4612  dmsn0el  5198  fidifsnen  7040  ctssdccl  7286  nninfwlpoimlemginf  7351  onntri35  7430  onntri45  7434  2omotaplemap  7451  exmidapne  7454  ltpopr  7790  caucvgprprlemnbj  7888  xrlttri3  10001  fzneuz  10305  iseqf1olemqcl  10729  iseqf1olemnab  10731  iseqf1olemab  10732  exp3val  10771  pwle2  16393