Theorem 3netr4d 3016

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ne 2939

This theorem is referenced by:  f1ounsn  7292  infpssrlem4  10344  modsumfzodifsn  13982  mgm2nsgrplem4  18947  pmtr3ncomlem1  19506  isdrng2  20760  prmirredlem  21501  uvcf1  21830  dfac14lem  23641  i1fmullem  25743  fta1glem1  26222  fta1blem  26225  plydivlem4  26353  fta1lem  26364  cubic  26907  asinlem  26926  dchrn0  27309  lgsne0  27394  noextenddif  27728  noresle  27757  perpneq  28737  axlowdimlem14  28985  preimane  32687  cycpmco2lem6  33134  cycpmrn  33146  irngnminplynz  33720  cntnevol  34209  subfacp1lem5  35169  fvtransport  36014  poimirlem1  37608  poimirlem6  37613  poimirlem7  37614  dalem4  39648  cdleme35sn2aw  40441  cdleme39n  40449  cdleme41fva11  40460  trlcone  40711  hdmaprnlem3N  41833  sticksstones2  42129  expeq1d  42338  uvcn0  42529  flt0  42624  stoweidlem23  45979  2zrngnmlid  48099  2zrngnmrid  48100  zlmodzxznm  48343  line2y  48605