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  6130  nnaordi  6654  iccf1o  10200  nnmindc  12555  ennnfonelemrn  12990  ctiunctlemfo  13010  sgrppropd  13446  mndpropd  13473  issubmnd  13475  imasgrp  13648  mulgnndir  13688  subg0cl  13719  subginvcl  13720  subgcl  13721  rngcl  13907  rngpropd  13918  srgcl  13933  srgidcl  13939  ringidcl  13983  ringpropd  14001  dvdsrd  14058  dvrvald  14098  subrngmcl  14173  subrgmcl  14197  subrgunit  14203  lmodprop2d  14312  lidl0  14453  lidl1  14454  psraddcl  14644  wlkl1loop  16069