Theorem 3netr4d 3036

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  f1ounsn  7306  infpssrlem4  10414  modsumfzodifsn  14117  mgm2nsgrplem4  19152  pmtr3ncomlem1  19720  isdrng2  21030  prmirredlem  21811  uvcf1  22131  dfac14lem  23969  i1fmullem  26048  fta1glem1  26519  fta1blem  26522  plydivlem4  26650  fta1lem  26661  cubic  27210  asinlem  27229  dchrn0  27610  lgsne0  27695  flt0  28002  fltoprm  28028  noextenddif  28058  noresle  28087  perpneq  29222  elcgrabasrd  29409  cgrabasimass  29411  axlowdimlem14  29566  preimane  33338  cycpmco2lem6  33768  cycpmrn  33780  ricnzr1  33925  psrnzr  34227  mplmulmvr  34254  irngnminplynz  34427  cntnevol  34944  subfacp1lem5  36129  fvtransport  36988  poimirlem1  38744  poimirlem6  38749  poimirlem7  38750  dalem4  40925  cdleme35sn2aw  41718  cdleme39n  41726  cdleme41fva11  41737  trlcone  41988  hdmaprnlem3N  43110  sticksstones2  43400  expeq1d  43585  uvcn0  43810  stoweidlem23  47248  gpg3kgrtriex  49402  gpgprismgr4cycllem7  49414  2zrngnmlid  49567  2zrngnmrid  49568  zlmodzxznm  49824  line2y  50082