Theorem sylnib 671

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 667	1 ⊢ (𝜑 → ¬ 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnibr  672  neqcomd  2175  inssdif0im  3482  undifexmid  4179  ordtriexmidlem2  4504  dmsn0el  5080  fidifsnen  6848  ctssdccl  7088  nninfwlpoimlemginf  7152  onntri35  7214  onntri45  7218  ltpopr  7557  caucvgprprlemnbj  7655  xrlttri3  9754  fzneuz  10057  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  exp3val  10478  pwle2  14031