Theorem 3eltr3d 2843

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

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

This theorem is referenced by:  axcc2lem  10396  axcclem  10417  icoshftf1o  13442  lincmb01cmp  13463  fzosubel  13692  symgsubmefmndALT  19340  psgnunilem1  19430  efgcpbllemb  19692  lspprabs  21009  cnmpt2res  23571  xpstopnlem1  23703  tususp  24166  tustps  24167  ressxms  24420  ressms  24421  tmsxpsval  24433  limcco  25801  dvcnp2  25828  dvcnp2OLD  25829  dvmulbr  25848  dvcobr  25856  dvcnvlem  25887  taylthlem2  26289  taylthlem2OLD  26290  jensen  26906  f1otrg  28805  nsgqusf1olem1  33391  txomap  33831  probmeasb  34428  fsum2dsub  34605  cvmlift2lem9  35305  prdsbnd2  37796  iocopn  45525  icoopn  45530  reclimc  45658  cncfiooicclem1  45898  itgiccshift  45985  dirkercncflem4  46111  fourierdlem32  46144  fourierdlem33  46145  fourierdlem60  46171  fourierdlem61  46172  fourierdlem76  46187  fourierdlem81  46192  fourierdlem90  46201  fourierdlem111  46222  uptrlem3  49205  fuco2eld3  49308  fucoid2  49342