Theorem tpeq123d 4070

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

Syntax hints:   -> wi 4   = wceq 1370   {ctp 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-un 3434  df-sn 3979  df-pr 3981  df-tp 3983

This theorem is referenced by:  fz0tp  11623  fzo0to3tp  11725  prdsval  14504  imasval  14560  fucval  14979  fucpropd  14998  setcval  15056  catcval  15075  xpcval  15098  symgval  15995  psrval  17544  om1val  20727  usgraexvlem  23458  rabren3dioph  29295  mendval  29681  ldualset  33079  erngfset  34752  erngfset-rN  34760  dvafset  34957  dvaset  34958  dvhfset  35034  dvhset  35035  hlhilset  35891