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

Theorem tpeq123d 4641
 Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
Hypotheses
Ref Expression
tpeq1d.1 (𝜑𝐴 = 𝐵)
tpeq123d.2 (𝜑𝐶 = 𝐷)
tpeq123d.3 (𝜑𝐸 = 𝐹)
Assertion
Ref Expression
tpeq123d (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})

Proof of Theorem tpeq123d
StepHypRef Expression
1 tpeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21tpeq1d 4638 . 2 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3 tpeq123d.2 . . 3 (𝜑𝐶 = 𝐷)
43tpeq2d 4639 . 2 (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5 tpeq123d.3 . . 3 (𝜑𝐸 = 𝐹)
65tpeq3d 4640 . 2 (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
72, 4, 63eqtrd 2797 1 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  {ctp 4526 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-sn 4523  df-pr 4525  df-tp 4527 This theorem is referenced by:  fz0tp  13057  fz0to4untppr  13059  fzo0to3tp  13172  fzo1to4tp  13174  prdsval  16786  imasval  16842  fucval  17287  fucpropd  17306  setcval  17403  catcval  17422  estrcval  17440  xpcval  17493  efmnd  18101  psrval  20677  om1val  23731  s3rn  30744  idlsrgval  31169  ldualset  36723  erngfset  38397  erngfset-rN  38405  dvafset  38602  dvaset  38603  dvhfset  38678  dvhset  38679  hlhilset  39532  rabren3dioph  40151  mendval  40522  nnsum4primesodd  44703  nnsum4primesoddALTV  44704  rngcvalALTV  44974  ringcvalALTV  45020
 Copyright terms: Public domain W3C validator