Theorem tpeq123d 4092

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

Syntax hints:   -> wi 4   = wceq 1438   {ctp 4001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442  df-sn 3998  df-pr 4000  df-tp 4002

This theorem is referenced by:  fz0tp  11895  fzo0to3tp  12000  prdsval  15346  imasval  15404  imasvalOLD  15405  fucval  15856  fucpropd  15875  setcval  15965  catcval  15984  estrcval  16002  xpcval  16055  symgval  17013  psrval  18579  om1val  22053  usgraexmplvtxlem  25114  ldualset  32654  erngfset  34329  erngfset-rN  34337  dvafset  34534  dvaset  34535  dvhfset  34611  dvhset  34612  hlhilset  35468  rabren3dioph  35621  mendval  36013  nnsum4primesodd  38647  nnsum4primesoddALTV  38648  rngcvalALTV  39305  ringcvalALTV  39351