Theorem 3eltr4d 2315

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  ovmpodxf  6157  nnaordi  6719  iccf1o  10301  ccatw2s1p1g  11288  nnmindc  12685  ennnfonelemrn  13120  ctiunctlemfo  13140  sgrppropd  13576  mndpropd  13603  issubmnd  13605  imasgrp  13778  mulgnndir  13818  subg0cl  13849  subginvcl  13850  subgcl  13851  rngcl  14038  rngpropd  14049  srgcl  14064  srgidcl  14070  ringidcl  14114  ringpropd  14132  dvdsrd  14189  dvrvald  14229  subrngmcl  14304  subrgmcl  14328  subrgunit  14334  lmodprop2d  14444  lidl0  14585  lidl1  14586  psraddcl  14781  wlkl1loop  16299  wlkres  16320  clwwlknonex2lem1  16378