Theorem eqnetrrid 3000

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  xpcoidgend  14900  fclsfnflim  23930  ptcmplem2  23956  vieta1lem1  26234  vieta1lem2  26235  fsuppcurry1  32681  fsuppcurry2  32682  constrresqrtcl  33746  signsvfpn  34555  signsvfnn  34556  finxpreclem2  37366  finxp1o  37368  cdleme3h  40217  cdleme7ga  40230  imo72b2lem0  44141  imo72b2lem1  44145  fourierdlem42  46134