Theorem eqnetrrid 3004

Description: A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypotheses

Ref	Expression
eqnetrrid.1	⊢ 𝐵 = 𝐴
eqnetrrid.2	⊢ (𝜑 → 𝐵 ≠ 𝐶)

Assertion

Ref	Expression
eqnetrrid	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Proof of Theorem eqnetrrid

Step	Hyp	Ref	Expression
1		eqnetrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqnetrrid.2	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
4	2, 3	eqnetrrd 2997	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  xpcoidgend  14889  fclsfnflim  23962  ptcmplem2  23988  vieta1lem1  26265  vieta1lem2  26266  fsuppcurry1  32731  fsuppcurry2  32732  constrresqrtcl  33862  signsvfpn  34670  signsvfnn  34671  finxpreclem2  37507  finxp1o  37509  cdleme3h  40407  cdleme7ga  40420  imo72b2lem0  44322  imo72b2lem1  44326  fourierdlem42  46309