Theorem 3netr4d 3033

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  f1ounsn  7272  infpssrlem4  10365  modsumfzodifsn  14067  mgm2nsgrplem4  19100  pmtr3ncomlem1  19667  isdrng2  20977  prmirredlem  21758  uvcf1  22078  dfac14lem  23916  i1fmullem  25995  fta1glem1  26466  fta1blem  26469  plydivlem4  26599  fta1lem  26610  cubic  27159  asinlem  27178  dchrn0  27559  lgsne0  27644  flt0  27951  fltoprm  27977  noextenddif  28007  noresle  28036  perpneq  29171  elcgrabasrd  29358  cgrabasimass  29360  axlowdimlem14  29515  preimane  33245  cycpmco2lem6  33674  cycpmrn  33686  ricnzr1  33831  psrnzr  34126  mplmulmvr  34153  irngnminplynz  34326  cntnevol  34843  subfacp1lem5  35918  fvtransport  36767  poimirlem1  38507  poimirlem6  38512  poimirlem7  38513  dalem4  40690  cdleme35sn2aw  41483  cdleme39n  41491  cdleme41fva11  41502  trlcone  41753  hdmaprnlem3N  42875  sticksstones2  43165  expeq1d  43349  uvcn0  43568  stoweidlem23  46977  gpg3kgrtriex  49131  gpgprismgr4cycllem7  49143  2zrngnmlid  49296  2zrngnmrid  49297  zlmodzxznm  49553  line2y  49811