Theorem 3eltr4d 2289

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  ovmpodxf  6073  nnaordi  6596  iccf1o  10128  nnmindc  12388  ennnfonelemrn  12823  ctiunctlemfo  12843  sgrppropd  13278  mndpropd  13305  issubmnd  13307  imasgrp  13480  mulgnndir  13520  subg0cl  13551  subginvcl  13552  subgcl  13553  rngcl  13739  rngpropd  13750  srgcl  13765  srgidcl  13771  ringidcl  13815  ringpropd  13833  dvdsrd  13889  dvrvald  13929  subrngmcl  14004  subrgmcl  14028  subrgunit  14034  lmodprop2d  14143  lidl0  14284  lidl1  14285  psraddcl  14475