Theorem eqnetrrid 3031

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 3024	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  xpcoidgend  14982  fclsfnflim  24075  ptcmplem2  24101  vieta1lem1  26362  vieta1lem2  26363  fsuppcurry1  32887  fsuppcurry2  32888  dflringlem3  33653  dflring4  33655  constrresqrtcl  34035  signsvfpn  34840  signsvfnn  34841  finxpreclem2  37845  finxp1o  37847  cdleme3h  40820  cdleme7ga  40833  imo72b2lem0  44702  imo72b2lem1  44706  fourierdlem42  46684