Theorem 3netr4d 3009

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

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

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 2707

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

This theorem is referenced by:  f1ounsn  7265  infpssrlem4  10320  modsumfzodifsn  13962  mgm2nsgrplem4  18899  pmtr3ncomlem1  19454  isdrng2  20703  prmirredlem  21433  uvcf1  21752  dfac14lem  23555  i1fmullem  25647  fta1glem1  26125  fta1blem  26128  plydivlem4  26256  fta1lem  26267  cubic  26811  asinlem  26830  dchrn0  27213  lgsne0  27298  noextenddif  27632  noresle  27661  perpneq  28693  axlowdimlem14  28934  preimane  32648  cycpmco2lem6  33142  cycpmrn  33154  irngnminplynz  33746  cntnevol  34259  subfacp1lem5  35206  fvtransport  36050  poimirlem1  37645  poimirlem6  37650  poimirlem7  37651  dalem4  39684  cdleme35sn2aw  40477  cdleme39n  40485  cdleme41fva11  40496  trlcone  40747  hdmaprnlem3N  41869  sticksstones2  42160  expeq1d  42373  uvcn0  42565  flt0  42660  stoweidlem23  46052  gpg3kgrtriex  48091  gpgprismgr4cycllem7  48100  2zrngnmlid  48230  2zrngnmrid  48231  zlmodzxznm  48473  line2y  48735