Theorem sylnib 687

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylnibr  688  neqcomd  2243  inssdif0imOLD  3593  undifexmid  4332  ordtriexmidlem2  4669  dmsn0el  5260  fidifsnen  7177  ctssdccl  7458  nninfwlpoimlemginf  7523  onntri35  7603  onntri45  7607  2omotaplemap  7630  exmidapne  7633  ltpopr  7969  caucvgprprlemnbj  8067  xrlttri3  10217  fzneuz  10526  iseqf1olemqcl  10958  iseqf1olemnab  10960  iseqf1olemab  10961  exp3val  11000  ballotfilemimin  13308  ballotfilemfrcn0  13332  psrlidmfi  15204  bposlem9  16331  pwle2  17245  wexmiddiffilem  17260  wexmiddifxylem  17262