Theorem 3netr4d 3003

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

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

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 2702

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

This theorem is referenced by:  f1ounsn  7250  infpssrlem4  10266  modsumfzodifsn  13916  mgm2nsgrplem4  18855  pmtr3ncomlem1  19410  isdrng2  20659  prmirredlem  21389  uvcf1  21708  dfac14lem  23511  i1fmullem  25602  fta1glem1  26080  fta1blem  26083  plydivlem4  26211  fta1lem  26222  cubic  26766  asinlem  26785  dchrn0  27168  lgsne0  27253  noextenddif  27587  noresle  27616  perpneq  28648  axlowdimlem14  28889  preimane  32601  cycpmco2lem6  33095  cycpmrn  33107  irngnminplynz  33709  cntnevol  34225  subfacp1lem5  35178  fvtransport  36027  poimirlem1  37622  poimirlem6  37627  poimirlem7  37628  dalem4  39666  cdleme35sn2aw  40459  cdleme39n  40467  cdleme41fva11  40478  trlcone  40729  hdmaprnlem3N  41851  sticksstones2  42142  expeq1d  42319  uvcn0  42537  flt0  42632  stoweidlem23  46028  gpg3kgrtriex  48084  gpgprismgr4cycllem7  48095  2zrngnmlid  48247  2zrngnmrid  48248  zlmodzxznm  48490  line2y  48748