Theorem 3eltr3d 2848

Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)

Hypotheses

Ref	Expression
3eltr3d.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
3eltr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eltr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eltr3d	⊢ (𝜑 → 𝐶 ∈ 𝐷)

Proof of Theorem 3eltr3d

Step	Hyp	Ref	Expression
1		3eltr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		3eltr3d.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
3		3eltr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	eleqtrd 2836	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
5	1, 4	eqeltrrd 2835	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  axcc2lem  10431  axcclem  10452  icoshftf1o  13451  lincmb01cmp  13472  fzosubel  13691  symgsubmefmndALT  19271  psgnunilem1  19361  efgcpbllemb  19623  lspprabs  20706  cnmpt2res  23181  xpstopnlem1  23313  tususp  23777  tustps  23778  ressxms  24034  ressms  24035  tmsxpsval  24047  limcco  25410  dvcnp2  25437  dvcnvlem  25493  taylthlem2  25886  jensen  26493  f1otrg  28122  nsgqusf1olem1  32524  txomap  32814  probmeasb  33429  fsum2dsub  33619  cvmlift2lem9  34302  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  prdsbnd2  36663  iocopn  44233  icoopn  44238  reclimc  44369  cncfiooicclem1  44609  itgiccshift  44696  dirkercncflem4  44822  fourierdlem32  44855  fourierdlem33  44856  fourierdlem60  44882  fourierdlem61  44883  fourierdlem76  44898  fourierdlem81  44903  fourierdlem90  44912  fourierdlem111  44933