Theorem 3eltr3d 2842

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  axcc2lem  10349  axcclem  10370  icoshftf1o  13395  lincmb01cmp  13416  fzosubel  13645  symgsubmefmndALT  19300  psgnunilem1  19390  efgcpbllemb  19652  lspprabs  21017  cnmpt2res  23580  xpstopnlem1  23712  tususp  24175  tustps  24176  ressxms  24429  ressms  24430  tmsxpsval  24442  limcco  25810  dvcnp2  25837  dvcnp2OLD  25838  dvmulbr  25857  dvcobr  25865  dvcnvlem  25896  taylthlem2  26298  taylthlem2OLD  26299  jensen  26915  f1otrg  28834  nsgqusf1olem1  33363  txomap  33803  probmeasb  34400  fsum2dsub  34577  cvmlift2lem9  35286  prdsbnd2  37777  iocopn  45505  icoopn  45510  reclimc  45638  cncfiooicclem1  45878  itgiccshift  45965  dirkercncflem4  46091  fourierdlem32  46124  fourierdlem33  46125  fourierdlem60  46151  fourierdlem61  46152  fourierdlem76  46167  fourierdlem81  46172  fourierdlem90  46181  fourierdlem111  46202  uptrlem3  49201  fuco2eld3  49304  fucoid2  49338