Theorem 3netr4d 3009

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

Syntax hints:   → wi 4   = wceq 1543   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-ne 2933

This theorem is referenced by:  infpssrlem4  9885  modsumfzodifsn  13482  mgm2nsgrplem4  18302  pmtr3ncomlem1  18819  isdrng2  19731  prmirredlem  20413  uvcf1  20708  dfac14lem  22468  i1fmullem  24545  fta1glem1  25017  fta1blem  25020  plydivlem4  25143  fta1lem  25154  cubic  25686  asinlem  25705  dchrn0  26085  lgsne0  26170  perpneq  26759  axlowdimlem14  27000  preimane  30681  cycpmco2lem6  31071  cycpmrn  31083  cntnevol  31862  subfacp1lem5  32813  noextenddif  33557  noresle  33586  fvtransport  34020  poimirlem1  35464  poimirlem6  35469  poimirlem7  35470  dalem4  37365  cdleme35sn2aw  38158  cdleme39n  38166  cdleme41fva11  38177  trlcone  38428  hdmaprnlem3N  39550  sticksstones2  39772  uvcn0  39918  flt0  40118  stoweidlem23  43182  2zrngnmlid  45123  2zrngnmrid  45124  zlmodzxznm  45454  line2y  45717