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

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