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

Theorem tpeq123d 4745
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 4742 . 2 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3 tpeq123d.2 . . 3 (𝜑𝐶 = 𝐷)
43tpeq2d 4743 . 2 (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5 tpeq123d.3 . . 3 (𝜑𝐸 = 𝐹)
65tpeq3d 4744 . 2 (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
72, 4, 63eqtrd 2775 1 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  {ctp 4626
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3949  df-sn 4623  df-pr 4625  df-tp 4627
This theorem is referenced by:  fz0tp  13584  fz0to4untppr  13586  fzo0to3tp  13700  fzo1to4tp  13702  prdsval  17383  imasval  17439  fucval  17892  fucpropd  17912  setcval  18009  catcval  18032  estrcval  18057  xpcval  18111  efmnd  18726  psrval  21399  om1val  24475  s3rn  31983  idlsrgval  32460  ldualset  37798  erngfset  39473  erngfset-rN  39481  dvafset  39678  dvaset  39679  dvhfset  39754  dvhset  39755  hlhilset  40608  rabren3dioph  41322  mendval  41694  oaun3  41901  nnsum4primesodd  46234  nnsum4primesoddALTV  46235  rngcvalALTV  46505  ringcvalALTV  46551  mndtcval  47351
  Copyright terms: Public domain W3C validator