Theorem tpeq123d 4109

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

Syntax hints:   -> wi 4   = wceq 1383   {ctp 4018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017  df-tp 4019

This theorem is referenced by:  fz0tp  11785  fzo0to3tp  11879  prdsval  14729  imasval  14785  fucval  15201  fucpropd  15220  setcval  15278  catcval  15297  xpcval  15320  symgval  16278  psrval  17885  om1val  21403  usgraexvlem  24267  rabren3dioph  30724  mendval  31108  estrcval  32479  rngcvalOLD  32509  ringcvalOLD  32552  ldualset  34590  erngfset  36265  erngfset-rN  36273  dvafset  36470  dvaset  36471  dvhfset  36547  dvhset  36548  hlhilset  37404