Theorem 3netr4d 3005

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  f1ounsn  7206  infpssrlem4  10197  modsumfzodifsn  13851  mgm2nsgrplem4  18829  pmtr3ncomlem1  19386  isdrng2  20659  prmirredlem  21410  uvcf1  21730  dfac14lem  23533  i1fmullem  25623  fta1glem1  26101  fta1blem  26104  plydivlem4  26232  fta1lem  26243  cubic  26787  asinlem  26806  dchrn0  27189  lgsne0  27274  noextenddif  27608  noresle  27637  perpneq  28693  axlowdimlem14  28934  preimane  32650  cycpmco2lem6  33098  cycpmrn  33110  irngnminplynz  33723  cntnevol  34239  subfacp1lem5  35226  fvtransport  36072  poimirlem1  37667  poimirlem6  37672  poimirlem7  37673  dalem4  39710  cdleme35sn2aw  40503  cdleme39n  40511  cdleme41fva11  40522  trlcone  40773  hdmaprnlem3N  41895  sticksstones2  42186  expeq1d  42363  uvcn0  42581  flt0  42676  stoweidlem23  46067  gpg3kgrtriex  48126  gpgprismgr4cycllem7  48138  2zrngnmlid  48292  2zrngnmrid  48293  zlmodzxznm  48535  line2y  48793