Theorem 3eltr4d 2277

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  ovmpodxf  6044  nnaordi  6561  iccf1o  10070  nnmindc  12171  ennnfonelemrn  12576  ctiunctlemfo  12596  sgrppropd  12996  mndpropd  13021  issubmnd  13023  imasgrp  13181  mulgnndir  13221  subg0cl  13252  subginvcl  13253  subgcl  13254  rngcl  13440  rngpropd  13451  srgcl  13466  srgidcl  13472  ringidcl  13516  ringpropd  13534  dvdsrd  13590  dvrvald  13630  subrngmcl  13705  subrgmcl  13729  subrgunit  13735  lmodprop2d  13844  lidl0  13985  lidl1  13986  psraddcl  14164