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  4278  ordtriexmidlem2  4613  dmsn0el  5201  fidifsnen  7045  ctssdccl  7294  nninfwlpoimlemginf  7359  onntri35  7438  onntri45  7442  2omotaplemap  7459  exmidapne  7462  ltpopr  7798  caucvgprprlemnbj  7896  xrlttri3  10010  fzneuz  10314  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemab  10741  exp3val  10780  pwle2  16477