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

Theorem tpeq123d 4057
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 4054 . 2  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  C ,  E } )
3 tpeq123d.2 . . 3  |-  ( ph  ->  C  =  D )
43tpeq2d 4055 . 2  |-  ( ph  ->  { B ,  C ,  E }  =  { B ,  D ,  E } )
5 tpeq123d.3 . . 3  |-  ( ph  ->  E  =  F )
65tpeq3d 4056 . 2  |-  ( ph  ->  { B ,  D ,  E }  =  { B ,  D ,  F } )
72, 4, 63eqtrd 2509 1  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  D ,  F } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452   {ctp 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-sn 3960  df-pr 3962  df-tp 3964
This theorem is referenced by:  fz0tp  11918  fzo0to3tp  12028  prdsval  15431  imasval  15489  imasvalOLD  15490  fucval  15941  fucpropd  15960  setcval  16050  catcval  16069  estrcval  16087  xpcval  16140  symgval  17098  psrval  18663  om1val  22139  usgraexmplvtxlem  25201  ldualset  32762  erngfset  34437  erngfset-rN  34445  dvafset  34642  dvaset  34643  dvhfset  34719  dvhset  34720  hlhilset  35576  rabren3dioph  35729  mendval  36120  nnsum4primesodd  39036  nnsum4primesoddALTV  39037  rngcvalALTV  40471  ringcvalALTV  40517
  Copyright terms: Public domain W3C validator