Theorem eqnetrrid 3014

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ne 2939

This theorem is referenced by:  xpcoidgend  15011  fclsfnflim  24051  ptcmplem2  24077  vieta1lem1  26367  vieta1lem2  26368  fsuppcurry1  32743  fsuppcurry2  32744  signsvfpn  34579  signsvfnn  34580  finxpreclem2  37373  finxp1o  37375  cdleme3h  40218  cdleme7ga  40231  imo72b2lem0  44155  imo72b2lem1  44159  fourierdlem42  46105