Theorem 3eltr3d 2853

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 2841	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
5	1, 4	eqeltrrd 2840	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  axcc2lem  10123  axcclem  10144  icoshftf1o  13135  lincmb01cmp  13156  fzosubel  13374  symgsubmefmndALT  18926  psgnunilem1  19016  efgcpbllemb  19276  lspprabs  20272  cnmpt2res  22736  xpstopnlem1  22868  tususp  23332  tustps  23333  ressxms  23587  ressms  23588  tmsxpsval  23600  limcco  24962  dvcnp2  24989  dvcnvlem  25045  taylthlem2  25438  jensen  26043  f1otrg  27136  nsgqusf1olem1  31500  txomap  31686  probmeasb  32297  fsum2dsub  32487  cvmlift2lem9  33173  prdsbnd2  35880  iocopn  42948  icoopn  42953  reclimc  43084  cncfiooicclem1  43324  itgiccshift  43411  dirkercncflem4  43537  fourierdlem32  43570  fourierdlem33  43571  fourierdlem60  43597  fourierdlem61  43598  fourierdlem76  43613  fourierdlem81  43618  fourierdlem90  43627  fourierdlem111  43648