Theorem 3netr4d 3016

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2938

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ne 2939

This theorem is referenced by:  infpssrlem4  10303  modsumfzodifsn  13913  mgm2nsgrplem4  18838  pmtr3ncomlem1  19382  isdrng2  20514  prmirredlem  21243  uvcf1  21566  dfac14lem  23341  i1fmullem  25443  fta1glem1  25918  fta1blem  25921  plydivlem4  26045  fta1lem  26056  cubic  26590  asinlem  26609  dchrn0  26989  lgsne0  27074  noextenddif  27407  noresle  27436  perpneq  28232  axlowdimlem14  28480  preimane  32162  cycpmco2lem6  32560  cycpmrn  32572  irngnminplynz  33060  cntnevol  33524  subfacp1lem5  34473  fvtransport  35308  poimirlem1  36792  poimirlem6  36797  poimirlem7  36798  dalem4  38839  cdleme35sn2aw  39632  cdleme39n  39640  cdleme41fva11  39651  trlcone  39902  hdmaprnlem3N  41024  sticksstones2  41269  uvcn0  41414  flt0  41681  stoweidlem23  45037  2zrngnmlid  46935  2zrngnmrid  46936  zlmodzxznm  47265  line2y  47528