Theorem 3netr4d 3010

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  f1ounsn  7228  infpssrlem4  10228  modsumfzodifsn  13879  mgm2nsgrplem4  18858  pmtr3ncomlem1  19414  isdrng2  20688  prmirredlem  21439  uvcf1  21759  dfac14lem  23573  i1fmullem  25663  fta1glem1  26141  fta1blem  26144  plydivlem4  26272  fta1lem  26283  cubic  26827  asinlem  26846  dchrn0  27229  lgsne0  27314  noextenddif  27648  noresle  27677  perpneq  28798  axlowdimlem14  29040  preimane  32758  cycpmco2lem6  33224  cycpmrn  33236  mplmulmvr  33715  irngnminplynz  33889  cntnevol  34405  subfacp1lem5  35397  fvtransport  36245  poimirlem1  37869  poimirlem6  37874  poimirlem7  37875  dalem4  40038  cdleme35sn2aw  40831  cdleme39n  40839  cdleme41fva11  40850  trlcone  41101  hdmaprnlem3N  42223  sticksstones2  42514  expeq1d  42691  uvcn0  42909  flt0  42992  stoweidlem23  46378  gpg3kgrtriex  48446  gpgprismgr4cycllem7  48458  2zrngnmlid  48612  2zrngnmrid  48613  zlmodzxznm  48854  line2y  49112