Theorem 3netr4d 3032

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  f1ounsn  7280  infpssrlem4  10387  modsumfzodifsn  14090  mgm2nsgrplem4  19125  pmtr3ncomlem1  19692  isdrng2  21002  prmirredlem  21783  uvcf1  22103  dfac14lem  23941  i1fmullem  26020  fta1glem1  26491  fta1blem  26494  plydivlem4  26622  fta1lem  26633  cubic  27182  asinlem  27201  dchrn0  27582  lgsne0  27667  flt0  27974  fltoprm  28000  noextenddif  28030  noresle  28059  perpneq  29194  elcgrabasrd  29381  cgrabasimass  29383  axlowdimlem14  29538  preimane  33310  cycpmco2lem6  33738  cycpmrn  33750  ricnzr1  33895  psrnzr  34190  mplmulmvr  34217  irngnminplynz  34390  cntnevol  34907  subfacp1lem5  36035  fvtransport  36889  poimirlem1  38632  poimirlem6  38637  poimirlem7  38638  dalem4  40815  cdleme35sn2aw  41608  cdleme39n  41616  cdleme41fva11  41627  trlcone  41878  hdmaprnlem3N  43000  sticksstones2  43290  expeq1d  43474  uvcn0  43699  stoweidlem23  47126  gpg3kgrtriex  49280  gpgprismgr4cycllem7  49292  2zrngnmlid  49445  2zrngnmrid  49446  zlmodzxznm  49702  line2y  49960