Theorem 3eltr3d 2877

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  axcc2lem  10421  axcclem  10442  icoshftf1o  13502  lincmb01cmp  13523  fzosubel  13755  symgsubmefmndALT  19474  psgnunilem1  19564  efgcpbllemb  19826  lspprabs  21197  cnmpt2res  23815  xpstopnlem1  23947  tususp  24409  tustps  24410  ressxms  24663  ressms  24664  tmsxpsval  24676  limcco  26033  dvcnp2  26060  dvmulbr  26079  dvcobr  26086  dvcnvlem  26116  taylthlem2  26518  jensen  27134  f1otrg  29201  nsgqusf1olem1  33703  txomap  34205  probmeasb  34801  fsum2dsub  34975  cvmlift2lem9  35784  nmulel1  36673  prdsbnd2  38427  iocopn  46219  icoopn  46224  reclimc  46350  cncfiooicclem1  46590  itgiccshift  46677  dirkercncflem4  46803  fourierdlem32  46836  fourierdlem33  46837  fourierdlem60  46863  fourierdlem61  46864  fourierdlem76  46879  fourierdlem81  46884  fourierdlem90  46893  fourierdlem111  46914  uptrlem3  49973  fuco2eld3  50076  fucoid2  50110