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  7247  infpssrlem4  10259  modsumfzodifsn  13909  mgm2nsgrplem4  18848  pmtr3ncomlem1  19403  isdrng2  20652  prmirredlem  21382  uvcf1  21701  dfac14lem  23504  i1fmullem  25595  fta1glem1  26073  fta1blem  26076  plydivlem4  26204  fta1lem  26215  cubic  26759  asinlem  26778  dchrn0  27161  lgsne0  27246  noextenddif  27580  noresle  27609  perpneq  28641  axlowdimlem14  28882  preimane  32594  cycpmco2lem6  33088  cycpmrn  33100  irngnminplynz  33702  cntnevol  34218  subfacp1lem5  35171  fvtransport  36020  poimirlem1  37615  poimirlem6  37620  poimirlem7  37621  dalem4  39659  cdleme35sn2aw  40452  cdleme39n  40460  cdleme41fva11  40471  trlcone  40722  hdmaprnlem3N  41844  sticksstones2  42135  expeq1d  42312  uvcn0  42530  flt0  42625  stoweidlem23  46021  gpg3kgrtriex  48080  gpgprismgr4cycllem7  48091  2zrngnmlid  48243  2zrngnmrid  48244  zlmodzxznm  48486  line2y  48744