Theorem eqnetrrid 3008

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

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

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 2708

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

This theorem is referenced by:  xpcoidgend  14999  fclsfnflim  23970  ptcmplem2  23996  vieta1lem1  26275  vieta1lem2  26276  fsuppcurry1  32707  fsuppcurry2  32708  constrresqrtcl  33816  signsvfpn  34622  signsvfnn  34623  finxpreclem2  37413  finxp1o  37415  cdleme3h  40259  cdleme7ga  40272  imo72b2lem0  44156  imo72b2lem1  44160  fourierdlem42  46145