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  10297  modsumfzodifsn  13905  mgm2nsgrplem4  18798  pmtr3ncomlem1  19334  isdrng2  20317  prmirredlem  21026  uvcf1  21331  dfac14lem  23103  i1fmullem  25193  fta1glem1  25665  fta1blem  25668  plydivlem4  25791  fta1lem  25802  cubic  26334  asinlem  26353  dchrn0  26733  lgsne0  26818  noextenddif  27151  noresle  27180  perpneq  27945  axlowdimlem14  28193  preimane  31873  cycpmco2lem6  32268  cycpmrn  32280  cntnevol  33164  subfacp1lem5  34113  fvtransport  34942  poimirlem1  36427  poimirlem6  36432  poimirlem7  36433  dalem4  38474  cdleme35sn2aw  39267  cdleme39n  39275  cdleme41fva11  39286  trlcone  39537  hdmaprnlem3N  40659  sticksstones2  40901  uvcn0  41062  flt0  41323  stoweidlem23  44674  2zrngnmlid  46749  2zrngnmrid  46750  zlmodzxznm  47080  line2y  47343