Theorem 3eltr4d 2280

Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)

Hypotheses

Ref	Expression
3eltr4d.1	|- ( ph -> A e. B )
3eltr4d.2	|- ( ph -> C = A )
3eltr4d.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3eltr4d	|- ( ph -> C e. D )

Proof of Theorem 3eltr4d

Step	Hyp	Ref	Expression
1		3eltr4d.2	. 2 |- ( ph -> C = A )
2		3eltr4d.1	. . 3 |- ( ph -> A e. B )
3		3eltr4d.3	. . 3 |- ( ph -> D = B )
4	2, 3	eleqtrrd 2276	. 2 |- ( ph -> A e. D )
5	1, 4	eqeltrd 2273	1 |- ( ph -> C e. D )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  ovmpodxf  6048  nnaordi  6566  iccf1o  10079  nnmindc  12201  ennnfonelemrn  12636  ctiunctlemfo  12656  sgrppropd  13056  mndpropd  13081  issubmnd  13083  imasgrp  13241  mulgnndir  13281  subg0cl  13312  subginvcl  13313  subgcl  13314  rngcl  13500  rngpropd  13511  srgcl  13526  srgidcl  13532  ringidcl  13576  ringpropd  13594  dvdsrd  13650  dvrvald  13690  subrngmcl  13765  subrgmcl  13789  subrgunit  13795  lmodprop2d  13904  lidl0  14045  lidl1  14046  psraddcl  14232