Theorem 3netr4d 3002

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  f1ounsn  7213  infpssrlem4  10219  modsumfzodifsn  13869  mgm2nsgrplem4  18813  pmtr3ncomlem1  19370  isdrng2  20646  prmirredlem  21397  uvcf1  21717  dfac14lem  23520  i1fmullem  25611  fta1glem1  26089  fta1blem  26092  plydivlem4  26220  fta1lem  26231  cubic  26775  asinlem  26794  dchrn0  27177  lgsne0  27262  noextenddif  27596  noresle  27625  perpneq  28677  axlowdimlem14  28918  preimane  32627  cycpmco2lem6  33086  cycpmrn  33098  irngnminplynz  33681  cntnevol  34197  subfacp1lem5  35159  fvtransport  36008  poimirlem1  37603  poimirlem6  37608  poimirlem7  37609  dalem4  39647  cdleme35sn2aw  40440  cdleme39n  40448  cdleme41fva11  40459  trlcone  40710  hdmaprnlem3N  41832  sticksstones2  42123  expeq1d  42300  uvcn0  42518  flt0  42613  stoweidlem23  46008  gpg3kgrtriex  48077  gpgprismgr4cycllem7  48089  2zrngnmlid  48243  2zrngnmrid  48244  zlmodzxznm  48486  line2y  48744