Theorem sylnib 683

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 679	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  684  neqcomd  2236  inssdif0im  3564  undifexmid  4289  ordtriexmidlem2  4624  dmsn0el  5213  fidifsnen  7100  ctssdccl  7353  nninfwlpoimlemginf  7418  onntri35  7498  onntri45  7502  2omotaplemap  7519  exmidapne  7522  ltpopr  7858  caucvgprprlemnbj  7956  xrlttri3  10075  fzneuz  10379  iseqf1olemqcl  10805  iseqf1olemnab  10807  iseqf1olemab  10808  exp3val  10847  pwle2  16700