MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tpeq123d Structured version   Unicode version

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
StepHypRef Expression
1 tpeq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21tpeq1d 4089 . 2  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  C ,  E } )
3 tpeq123d.2 . . 3  |-  ( ph  ->  C  =  D )
43tpeq2d 4090 . 2  |-  ( ph  ->  { B ,  C ,  E }  =  { B ,  D ,  E } )
5 tpeq123d.3 . . 3  |-  ( ph  ->  E  =  F )
65tpeq3d 4091 . 2  |-  ( ph  ->  { B ,  D ,  E }  =  { B ,  D ,  F } )
72, 4, 63eqtrd 2468 1  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  D ,  F } )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator