Theorem 3eltr3d 2847

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  axcc2lem  10433  axcclem  10454  icoshftf1o  13453  lincmb01cmp  13474  fzosubel  13693  symgsubmefmndALT  19273  psgnunilem1  19363  efgcpbllemb  19625  lspprabs  20711  cnmpt2res  23188  xpstopnlem1  23320  tususp  23784  tustps  23785  ressxms  24041  ressms  24042  tmsxpsval  24054  limcco  25417  dvcnp2  25444  dvcnvlem  25500  taylthlem2  25893  jensen  26500  f1otrg  28160  nsgqusf1olem1  32569  txomap  32883  probmeasb  33498  fsum2dsub  33688  cvmlift2lem9  34371  gg-dvcnp2  35243  gg-dvmulbr  35244  gg-dvcobr  35245  prdsbnd2  36749  iocopn  44312  icoopn  44317  reclimc  44448  cncfiooicclem1  44688  itgiccshift  44775  dirkercncflem4  44901  fourierdlem32  44934  fourierdlem33  44935  fourierdlem60  44961  fourierdlem61  44962  fourierdlem76  44977  fourierdlem81  44982  fourierdlem90  44991  fourierdlem111  45012