Theorem 3netr4d 3018

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  f1ounsn  7292  infpssrlem4  10346  modsumfzodifsn  13985  mgm2nsgrplem4  18934  pmtr3ncomlem1  19491  isdrng2  20743  prmirredlem  21483  uvcf1  21812  dfac14lem  23625  i1fmullem  25729  fta1glem1  26207  fta1blem  26210  plydivlem4  26338  fta1lem  26349  cubic  26892  asinlem  26911  dchrn0  27294  lgsne0  27379  noextenddif  27713  noresle  27742  perpneq  28722  axlowdimlem14  28970  preimane  32680  cycpmco2lem6  33151  cycpmrn  33163  irngnminplynz  33755  cntnevol  34229  subfacp1lem5  35189  fvtransport  36033  poimirlem1  37628  poimirlem6  37633  poimirlem7  37634  dalem4  39667  cdleme35sn2aw  40460  cdleme39n  40468  cdleme41fva11  40479  trlcone  40730  hdmaprnlem3N  41852  sticksstones2  42148  expeq1d  42359  uvcn0  42552  flt0  42647  stoweidlem23  46038  gpg3kgrtriex  48045  2zrngnmlid  48171  2zrngnmrid  48172  zlmodzxznm  48414  line2y  48676