Theorem 3netr4d 3006

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2929

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 2705

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

This theorem is referenced by:  f1ounsn  7214  infpssrlem4  10206  modsumfzodifsn  13855  mgm2nsgrplem4  18833  pmtr3ncomlem1  19389  isdrng2  20662  prmirredlem  21413  uvcf1  21733  dfac14lem  23535  i1fmullem  25625  fta1glem1  26103  fta1blem  26106  plydivlem4  26234  fta1lem  26245  cubic  26789  asinlem  26808  dchrn0  27191  lgsne0  27276  noextenddif  27610  noresle  27639  perpneq  28695  axlowdimlem14  28937  preimane  32656  cycpmco2lem6  33109  cycpmrn  33121  mplmulmvr  33592  irngnminplynz  33748  cntnevol  34264  subfacp1lem5  35251  fvtransport  36099  poimirlem1  37684  poimirlem6  37689  poimirlem7  37690  dalem4  39787  cdleme35sn2aw  40580  cdleme39n  40588  cdleme41fva11  40599  trlcone  40850  hdmaprnlem3N  41972  sticksstones2  42263  expeq1d  42445  uvcn0  42663  flt0  42758  stoweidlem23  46148  gpg3kgrtriex  48216  gpgprismgr4cycllem7  48228  2zrngnmlid  48382  2zrngnmrid  48383  zlmodzxznm  48625  line2y  48883