Theorem 3eltr3d 2858

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  axcc2lem  10505  axcclem  10526  icoshftf1o  13534  lincmb01cmp  13555  fzosubel  13775  symgsubmefmndALT  19445  psgnunilem1  19535  efgcpbllemb  19797  lspprabs  21117  cnmpt2res  23706  xpstopnlem1  23838  tususp  24302  tustps  24303  ressxms  24559  ressms  24560  tmsxpsval  24572  limcco  25948  dvcnp2  25975  dvcnp2OLD  25976  dvmulbr  25995  dvcobr  26003  dvcnvlem  26034  taylthlem2  26434  taylthlem2OLD  26435  jensen  27050  f1otrg  28897  nsgqusf1olem1  33406  txomap  33780  probmeasb  34395  fsum2dsub  34584  cvmlift2lem9  35279  prdsbnd2  37755  iocopn  45438  icoopn  45443  reclimc  45574  cncfiooicclem1  45814  itgiccshift  45901  dirkercncflem4  46027  fourierdlem32  46060  fourierdlem33  46061  fourierdlem60  46087  fourierdlem61  46088  fourierdlem76  46103  fourierdlem81  46108  fourierdlem90  46117  fourierdlem111  46138