Theorem 3netr4d 3038

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962

This theorem is used by:  f1ounsn  7281  infpssrlem4  10308  modsumfzodifsn  14000  mgm2nsgrplem4  19014  pmtr3ncomlem1  19574  isdrng2  20880  prmirredlem  21659  uvcf1  21979  dfac14lem  23811  i1fmullem  25890  fta1glem1  26362  fta1blem  26365  plydivlem4  26494  fta1lem  26505  cubic  27051  asinlem  27070  dchrn0  27451  lgsne0  27536  noextenddif  27869  noresle  27898  perpneq  29031  axlowdimlem14  29342  preimane  33051  cycpmco2lem6  33482  cycpmrn  33494  ricnzr1  33639  psrnzr  33933  mplmulmvr  33960  irngnminplynz  34133  cntnevol  34650  subfacp1lem5  35697  fvtransport  36545  mh-inf3f1  37093  poimirlem1  38313  poimirlem6  38318  poimirlem7  38319  dalem4  40480  cdleme35sn2aw  41273  cdleme39n  41281  cdleme41fva11  41292  trlcone  41543  hdmaprnlem3N  42665  sticksstones2  42955  expeq1d  43126  uvcn0  43351  flt0  43410  stoweidlem23  46778  gpg3kgrtriex  48895  gpgprismgr4cycllem7  48907  2zrngnmlid  49061  2zrngnmrid  49062  zlmodzxznm  49318  line2y  49576