Theorem 3netr4d 3037

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

Syntax hints:   → wi 4   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  f1ounsn  7260  infpssrlem4  10278  modsumfzodifsn  13968  mgm2nsgrplem4  18971  pmtr3ncomlem1  19531  isdrng2  20815  prmirredlem  21579  uvcf1  21899  dfac14lem  23731  i1fmullem  25810  fta1glem1  26282  fta1blem  26285  plydivlem4  26414  fta1lem  26425  cubic  26968  asinlem  26987  dchrn0  27368  lgsne0  27453  noextenddif  27786  noresle  27815  perpneq  28941  axlowdimlem14  29210  preimane  32922  cycpmco2lem6  33359  cycpmrn  33371  ricnzr1  33516  psrnzr  33814  mplmulmvr  33841  irngnminplynz  34014  cntnevol  34530  subfacp1lem5  35542  fvtransport  36390  mh-inf3f1  36909  poimirlem1  38127  poimirlem6  38132  poimirlem7  38133  dalem4  40296  cdleme35sn2aw  41089  cdleme39n  41097  cdleme41fva11  41108  trlcone  41359  hdmaprnlem3N  42481  sticksstones2  42771  expeq1d  42940  uvcn0  43167  flt0  43226  stoweidlem23  46596  gpg3kgrtriex  48710  gpgprismgr4cycllem7  48722  2zrngnmlid  48876  2zrngnmrid  48877  zlmodzxznm  49129  line2y  49387