Theorem tpeq123d 4057

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 4054	. 2 |- ( ph -> { A , C , E } = { B , C , E } )
3		tpeq123d.2	. . 3 |- ( ph -> C = D )
4	3	tpeq2d 4055	. 2 |- ( ph -> { B , C , E } = { B , D , E } )
5		tpeq123d.3	. . 3 |- ( ph -> E = F )
6	5	tpeq3d 4056	. 2 |- ( ph -> { B , D , E } = { B , D , F } )
7	2, 4, 6	3eqtrd 2509	1 |- ( ph -> { A , C , E } = { B , D , F } )

Syntax hints:   -> wi 4   = wceq 1452   {ctp 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-sn 3960  df-pr 3962  df-tp 3964

This theorem is referenced by:  fz0tp  11918  fzo0to3tp  12028  prdsval  15431  imasval  15489  imasvalOLD  15490  fucval  15941  fucpropd  15960  setcval  16050  catcval  16069  estrcval  16087  xpcval  16140  symgval  17098  psrval  18663  om1val  22139  usgraexmplvtxlem  25201  ldualset  32762  erngfset  34437  erngfset-rN  34445  dvafset  34642  dvaset  34643  dvhfset  34719  dvhset  34720  hlhilset  35576  rabren3dioph  35729  mendval  36120  nnsum4primesodd  39036  nnsum4primesoddALTV  39037  rngcvalALTV  40471  ringcvalALTV  40517