Theorem 3netr4d 3034

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  f1ounsn  7277  infpssrlem4  10312  modsumfzodifsn  14012  mgm2nsgrplem4  19039  pmtr3ncomlem1  19606  isdrng2  20912  prmirredlem  21691  uvcf1  22011  dfac14lem  23849  i1fmullem  25928  fta1glem1  26400  fta1blem  26403  plydivlem4  26533  fta1lem  26544  cubic  27094  asinlem  27113  dchrn0  27494  lgsne0  27579  noextenddif  27912  noresle  27941  perpneq  29076  elcgrabasrd  29263  cgrabasimass  29265  axlowdimlem14  29420  preimane  33150  cycpmco2lem6  33579  cycpmrn  33591  ricnzr1  33736  psrnzr  34030  mplmulmvr  34057  irngnminplynz  34230  cntnevol  34747  subfacp1lem5  35771  fvtransport  36620  mh-inf3f1  37168  poimirlem1  38378  poimirlem6  38383  poimirlem7  38384  dalem4  40546  cdleme35sn2aw  41339  cdleme39n  41347  cdleme41fva11  41358  trlcone  41609  hdmaprnlem3N  42731  sticksstones2  43021  expeq1d  43207  uvcn0  43432  flt0  43491  stoweidlem23  46859  gpg3kgrtriex  49013  gpgprismgr4cycllem7  49025  2zrngnmlid  49178  2zrngnmrid  49179  zlmodzxznm  49435  line2y  49693