Theorem sylnib 678

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 674	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  679  neqcomd  2211  inssdif0im  3530  undifexmid  4242  ordtriexmidlem2  4573  dmsn0el  5158  fidifsnen  6979  ctssdccl  7225  nninfwlpoimlemginf  7290  onntri35  7362  onntri45  7366  2omotaplemap  7382  exmidapne  7385  ltpopr  7721  caucvgprprlemnbj  7819  xrlttri3  9932  fzneuz  10236  iseqf1olemqcl  10657  iseqf1olemnab  10659  iseqf1olemab  10660  exp3val  10699  pwle2  16050