Theorem 3eltr4d 2313

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 2309	. 2 |- ( ph -> A e. D )
5	1, 4	eqeltrd 2306	1 |- ( ph -> C e. D )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  ovmpodxf  6136  nnaordi  6662  iccf1o  10212  nnmindc  12571  ennnfonelemrn  13006  ctiunctlemfo  13026  sgrppropd  13462  mndpropd  13489  issubmnd  13491  imasgrp  13664  mulgnndir  13704  subg0cl  13735  subginvcl  13736  subgcl  13737  rngcl  13923  rngpropd  13934  srgcl  13949  srgidcl  13955  ringidcl  13999  ringpropd  14017  dvdsrd  14074  dvrvald  14114  subrngmcl  14189  subrgmcl  14213  subrgunit  14219  lmodprop2d  14328  lidl0  14469  lidl1  14470  psraddcl  14660  wlkl1loop  16104  wlkres  16123