Theorem 3netr4d 3095

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-ne 3019

This theorem is referenced by:  infpssrlem4  9730  modsumfzodifsn  13315  mgm2nsgrplem4  18088  pmtr3ncomlem1  18603  isdrng2  19514  prmirredlem  20642  uvcf1  20938  dfac14lem  22227  i1fmullem  24297  fta1glem1  24761  fta1blem  24764  plydivlem4  24887  fta1lem  24898  cubic  25429  asinlem  25448  dchrn0  25828  lgsne0  25913  perpneq  26502  axlowdimlem14  26743  preimane  30417  cycpmco2lem6  30775  cycpmrn  30787  cntnevol  31489  subfacp1lem5  32433  noextenddif  33177  noresle  33202  fvtransport  33495  poimirlem1  34895  poimirlem6  34900  poimirlem7  34901  dalem4  36803  cdleme35sn2aw  37596  cdleme39n  37604  cdleme41fva11  37615  trlcone  37866  hdmaprnlem3N  38988  uvcn0  39158  stoweidlem23  42315  2zrngnmlid  44227  2zrngnmrid  44228  zlmodzxznm  44559  line2y  44749