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  2198  inssdif0im  3514  undifexmid  4222  ordtriexmidlem2  4552  dmsn0el  5135  fidifsnen  6926  ctssdccl  7170  nninfwlpoimlemginf  7235  onntri35  7297  onntri45  7301  2omotaplemap  7317  exmidapne  7320  ltpopr  7655  caucvgprprlemnbj  7753  xrlttri3  9863  fzneuz  10167  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  exp3val  10612  pwle2  15489