Theorem tpeq123d 4069

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

Syntax hints:   -> wi 4   = wceq 1446   {ctp 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-un 3411  df-sn 3971  df-pr 3973  df-tp 3975

This theorem is referenced by:  fz0tp  11900  fzo0to3tp  12006  prdsval  15365  imasval  15423  imasvalOLD  15424  fucval  15875  fucpropd  15894  setcval  15984  catcval  16003  estrcval  16021  xpcval  16074  symgval  17032  psrval  18598  om1val  22073  usgraexmplvtxlem  25134  ldualset  32703  erngfset  34378  erngfset-rN  34386  dvafset  34583  dvaset  34584  dvhfset  34660  dvhset  34661  hlhilset  35517  rabren3dioph  35670  mendval  36061  nnsum4primesodd  38901  nnsum4primesoddALTV  38902  rngcvalALTV  40067  ringcvalALTV  40113