Theorem 3netr4d 3020

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  infpssrlem4  9993  modsumfzodifsn  13592  mgm2nsgrplem4  18475  pmtr3ncomlem1  18996  isdrng2  19916  prmirredlem  20606  uvcf1  20909  dfac14lem  22676  i1fmullem  24763  fta1glem1  25235  fta1blem  25238  plydivlem4  25361  fta1lem  25372  cubic  25904  asinlem  25923  dchrn0  26303  lgsne0  26388  perpneq  26979  axlowdimlem14  27226  preimane  30909  cycpmco2lem6  31300  cycpmrn  31312  cntnevol  32096  subfacp1lem5  33046  noextenddif  33798  noresle  33827  fvtransport  34261  poimirlem1  35705  poimirlem6  35710  poimirlem7  35711  dalem4  37606  cdleme35sn2aw  38399  cdleme39n  38407  cdleme41fva11  38418  trlcone  38669  hdmaprnlem3N  39791  sticksstones2  40031  uvcn0  40190  flt0  40390  stoweidlem23  43454  2zrngnmlid  45395  2zrngnmrid  45396  zlmodzxznm  45726  line2y  45989