Theorem 3netr4d 3010

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 3000	. 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
4		3netr4d.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	neeqtrrd 3007	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  f1ounsn  7218  infpssrlem4  10217  modsumfzodifsn  13895  mgm2nsgrplem4  18881  pmtr3ncomlem1  19437  isdrng2  20709  prmirredlem  21460  uvcf1  21780  dfac14lem  23591  i1fmullem  25670  fta1glem1  26145  fta1blem  26148  plydivlem4  26275  fta1lem  26286  cubic  26830  asinlem  26849  dchrn0  27232  lgsne0  27317  noextenddif  27651  noresle  27680  perpneq  28801  axlowdimlem14  29043  preimane  32762  cycpmco2lem6  33212  cycpmrn  33224  mplmulmvr  33703  irngnminplynz  33877  cntnevol  34393  subfacp1lem5  35387  fvtransport  36235  poimirlem1  37953  poimirlem6  37958  poimirlem7  37959  dalem4  40122  cdleme35sn2aw  40915  cdleme39n  40923  cdleme41fva11  40934  trlcone  41185  hdmaprnlem3N  42307  sticksstones2  42597  expeq1d  42767  uvcn0  42998  flt0  43081  stoweidlem23  46466  gpg3kgrtriex  48562  gpgprismgr4cycllem7  48574  2zrngnmlid  48728  2zrngnmrid  48729  zlmodzxznm  48970  line2y  49228