Theorem 3netr4d 3024

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  infpssrlem4  10375  modsumfzodifsn  13995  mgm2nsgrplem4  18956  pmtr3ncomlem1  19515  isdrng2  20765  prmirredlem  21506  uvcf1  21835  dfac14lem  23646  i1fmullem  25748  fta1glem1  26227  fta1blem  26230  plydivlem4  26356  fta1lem  26367  cubic  26910  asinlem  26929  dchrn0  27312  lgsne0  27397  noextenddif  27731  noresle  27760  perpneq  28740  axlowdimlem14  28988  preimane  32688  cycpmco2lem6  33124  cycpmrn  33136  irngnminplynz  33705  cntnevol  34192  subfacp1lem5  35152  fvtransport  35996  poimirlem1  37581  poimirlem6  37586  poimirlem7  37587  dalem4  39622  cdleme35sn2aw  40415  cdleme39n  40423  cdleme41fva11  40434  trlcone  40685  hdmaprnlem3N  41807  sticksstones2  42104  expeq1d  42311  uvcn0  42497  flt0  42592  stoweidlem23  45944  2zrngnmlid  47978  2zrngnmrid  47979  zlmodzxznm  48226  line2y  48489