Theorem 3netr4d 3035

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  f1ounsn  7272  infpssrlem4  10291  modsumfzodifsn  13982  mgm2nsgrplem4  18984  pmtr3ncomlem1  19544  isdrng2  20830  prmirredlem  21603  uvcf1  21923  dfac14lem  23755  i1fmullem  25834  fta1glem1  26306  fta1blem  26309  plydivlem4  26438  fta1lem  26449  cubic  26995  asinlem  27014  dchrn0  27395  lgsne0  27480  noextenddif  27813  noresle  27842  perpneq  28975  axlowdimlem14  29286  preimane  32995  cycpmco2lem6  33432  cycpmrn  33444  ricnzr1  33589  psrnzr  33883  mplmulmvr  33910  irngnminplynz  34083  cntnevol  34599  subfacp1lem5  35657  fvtransport  36505  mh-inf3f1  37033  poimirlem1  38253  poimirlem6  38258  poimirlem7  38259  dalem4  40420  cdleme35sn2aw  41213  cdleme39n  41221  cdleme41fva11  41232  trlcone  41483  hdmaprnlem3N  42605  sticksstones2  42895  expeq1d  43066  uvcn0  43293  flt0  43352  stoweidlem23  46720  gpg3kgrtriex  48837  gpgprismgr4cycllem7  48849  2zrngnmlid  49003  2zrngnmrid  49004  zlmodzxznm  49260  line2y  49518