Theorem 3netr4d 3019

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  infpssrlem4  10301  modsumfzodifsn  13909  mgm2nsgrplem4  18802  pmtr3ncomlem1  19341  isdrng2  20371  prmirredlem  21042  uvcf1  21347  dfac14lem  23121  i1fmullem  25211  fta1glem1  25683  fta1blem  25686  plydivlem4  25809  fta1lem  25820  cubic  26354  asinlem  26373  dchrn0  26753  lgsne0  26838  noextenddif  27171  noresle  27200  perpneq  27965  axlowdimlem14  28213  preimane  31895  cycpmco2lem6  32290  cycpmrn  32302  irngnminplynz  32771  cntnevol  33226  subfacp1lem5  34175  fvtransport  35004  poimirlem1  36489  poimirlem6  36494  poimirlem7  36495  dalem4  38536  cdleme35sn2aw  39329  cdleme39n  39337  cdleme41fva11  39348  trlcone  39599  hdmaprnlem3N  40721  sticksstones2  40963  uvcn0  41112  flt0  41379  stoweidlem23  44739  2zrngnmlid  46847  2zrngnmrid  46848  zlmodzxznm  47178  line2y  47441