Theorem tpeq123d 4038

Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)

Hypotheses

Ref	Expression
tpeq1d.1	|- ( ph -> A = B )
tpeq123d.2	|- ( ph -> C = D )
tpeq123d.3	|- ( ph -> E = F )

Assertion

Ref	Expression
tpeq123d	|- ( ph -> { A , C , E } = { B , D , F } )

Proof of Theorem tpeq123d

Step	Hyp	Ref	Expression
1		tpeq1d.1	. . 3 |- ( ph -> A = B )
2	1	tpeq1d 4035	. 2 |- ( ph -> { A , C , E } = { B , C , E } )
3		tpeq123d.2	. . 3 |- ( ph -> C = D )
4	3	tpeq2d 4036	. 2 |- ( ph -> { B , C , E } = { B , D , E } )
5		tpeq123d.3	. . 3 |- ( ph -> E = F )
6	5	tpeq3d 4037	. 2 |- ( ph -> { B , D , E } = { B , D , F } )
7	2, 4, 6	3eqtrd 2427	1 |- ( ph -> { A , C , E } = { B , D , F } )

Syntax hints:   -> wi 4   = wceq 1399   {ctp 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-un 3394  df-sn 3945  df-pr 3947  df-tp 3949

This theorem is referenced by:  fz0tp  11699  fzo0to3tp  11799  prdsval  14862  imasval  14918  fucval  15364  fucpropd  15383  setcval  15473  catcval  15492  estrcval  15510  xpcval  15563  symgval  16521  psrval  18124  om1val  21615  usgraexvlem  24516  rabren3dioph  30914  mendval  31300  rngcvalALTV  32969  ringcvalALTV  33015  ldualset  35263  erngfset  36938  erngfset-rN  36946  dvafset  37143  dvaset  37144  dvhfset  37220  dvhset  37221  hlhilset  38077