Theorem 3netr4d 3033

Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 21-Nov-2019.)

Hypotheses

Ref	Expression
3netr4d.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
3netr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3netr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3netr4d	⊢ (𝜑 → 𝐶 ≠ 𝐷)

Proof of Theorem 3netr4d

Step	Hyp	Ref	Expression
1		3netr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3netr4d.1	. . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
3	1, 2	eqnetrd 3023	. 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
4		3netr4d.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	neeqtrrd 3030	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:  f1ounsn  7252  infpssrlem4  10260  modsumfzodifsn  13954  mgm2nsgrplem4  18941  pmtr3ncomlem1  19496  isdrng2  20772  prmirredlem  21504  uvcf1  21824  dfac14lem  23657  i1fmullem  25736  fta1glem1  26208  fta1blem  26211  plydivlem4  26337  fta1lem  26348  cubic  26891  asinlem  26910  dchrn0  27291  lgsne0  27376  noextenddif  27709  noresle  27738  perpneq  28860  axlowdimlem14  29102  preimane  32821  cycpmco2lem6  33272  cycpmrn  33284  ricnzr1  33433  psrnzr  33770  mplmulmvr  33797  irngnminplynz  33970  cntnevol  34486  subfacp1lem5  35498  fvtransport  36346  mh-inf3f1  36865  poimirlem1  38084  poimirlem6  38089  poimirlem7  38090  dalem4  40253  cdleme35sn2aw  41046  cdleme39n  41054  cdleme41fva11  41065  trlcone  41316  hdmaprnlem3N  42438  sticksstones2  42728  expeq1d  42897  uvcn0  43124  flt0  43183  stoweidlem23  46561  gpg3kgrtriex  48675  gpgprismgr4cycllem7  48687  2zrngnmlid  48841  2zrngnmrid  48842  zlmodzxznm  49083  line2y  49341