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 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  f1ounsn  7218  infpssrlem4  10216  modsumfzodifsn  13867  mgm2nsgrplem4  18846  pmtr3ncomlem1  19402  isdrng2  20676  prmirredlem  21427  uvcf1  21747  dfac14lem  23561  i1fmullem  25651  fta1glem1  26129  fta1blem  26132  plydivlem4  26260  fta1lem  26271  cubic  26815  asinlem  26834  dchrn0  27217  lgsne0  27302  noextenddif  27636  noresle  27665  perpneq  28786  axlowdimlem14  29028  preimane  32748  cycpmco2lem6  33213  cycpmrn  33225  mplmulmvr  33704  irngnminplynz  33869  cntnevol  34385  subfacp1lem5  35378  fvtransport  36226  poimirlem1  37822  poimirlem6  37827  poimirlem7  37828  dalem4  39925  cdleme35sn2aw  40718  cdleme39n  40726  cdleme41fva11  40737  trlcone  40988  hdmaprnlem3N  42110  sticksstones2  42401  expeq1d  42579  uvcn0  42797  flt0  42880  stoweidlem23  46267  gpg3kgrtriex  48335  gpgprismgr4cycllem7  48347  2zrngnmlid  48501  2zrngnmrid  48502  zlmodzxznm  48743  line2y  49001