Theorem 3netr4d 3021

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

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

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  infpssrlem4  10062  modsumfzodifsn  13664  mgm2nsgrplem4  18560  pmtr3ncomlem1  19081  isdrng2  20001  prmirredlem  20694  uvcf1  20999  dfac14lem  22768  i1fmullem  24858  fta1glem1  25330  fta1blem  25333  plydivlem4  25456  fta1lem  25467  cubic  25999  asinlem  26018  dchrn0  26398  lgsne0  26483  perpneq  27075  axlowdimlem14  27323  preimane  31007  cycpmco2lem6  31398  cycpmrn  31410  cntnevol  32196  subfacp1lem5  33146  noextenddif  33871  noresle  33900  fvtransport  34334  poimirlem1  35778  poimirlem6  35783  poimirlem7  35784  dalem4  37679  cdleme35sn2aw  38472  cdleme39n  38480  cdleme41fva11  38491  trlcone  38742  hdmaprnlem3N  39864  sticksstones2  40103  uvcn0  40265  flt0  40474  stoweidlem23  43564  2zrngnmlid  45507  2zrngnmrid  45508  zlmodzxznm  45838  line2y  46101