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  10389  axcclem  10410  icoshftf1o  13435  lincmb01cmp  13456  fzosubel  13685  symgsubmefmndALT  19333  psgnunilem1  19423  efgcpbllemb  19685  lspprabs  21002  cnmpt2res  23564  xpstopnlem1  23696  tususp  24159  tustps  24160  ressxms  24413  ressms  24414  tmsxpsval  24426  limcco  25794  dvcnp2  25821  dvcnp2OLD  25822  dvmulbr  25841  dvcobr  25849  dvcnvlem  25880  taylthlem2  26282  taylthlem2OLD  26283  jensen  26899  f1otrg  28798  nsgqusf1olem1  33384  txomap  33824  probmeasb  34421  fsum2dsub  34598  cvmlift2lem9  35298  prdsbnd2  37789  iocopn  45518  icoopn  45523  reclimc  45651  cncfiooicclem1  45891  itgiccshift  45978  dirkercncflem4  46104  fourierdlem32  46137  fourierdlem33  46138  fourierdlem60  46164  fourierdlem61  46165  fourierdlem76  46180  fourierdlem81  46185  fourierdlem90  46194  fourierdlem111  46215  uptrlem3  49201  fuco2eld3  49304  fucoid2  49338