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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  f1ounsn  7227  infpssrlem4  10228  modsumfzodifsn  13906  mgm2nsgrplem4  18892  pmtr3ncomlem1  19448  isdrng2  20720  prmirredlem  21452  uvcf1  21772  dfac14lem  23582  i1fmullem  25661  fta1glem1  26133  fta1blem  26136  plydivlem4  26262  fta1lem  26273  cubic  26813  asinlem  26832  dchrn0  27213  lgsne0  27298  noextenddif  27632  noresle  27661  perpneq  28782  axlowdimlem14  29024  preimane  32742  cycpmco2lem6  33192  cycpmrn  33204  mplmulmvr  33683  irngnminplynz  33856  cntnevol  34372  subfacp1lem5  35366  fvtransport  36214  mh-inf3f1  36723  poimirlem1  37942  poimirlem6  37947  poimirlem7  37948  dalem4  40111  cdleme35sn2aw  40904  cdleme39n  40912  cdleme41fva11  40923  trlcone  41174  hdmaprnlem3N  42296  sticksstones2  42586  expeq1d  42756  uvcn0  42987  flt0  43070  stoweidlem23  46451  gpg3kgrtriex  48565  gpgprismgr4cycllem7  48577  2zrngnmlid  48731  2zrngnmrid  48732  zlmodzxznm  48973  line2y  49231