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

Theorem tpeq123d 4258
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 4255 . 2 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3 tpeq123d.2 . . 3 (𝜑𝐶 = 𝐷)
43tpeq2d 4256 . 2 (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5 tpeq123d.3 . . 3 (𝜑𝐸 = 𝐹)
65tpeq3d 4257 . 2 (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
72, 4, 63eqtrd 2664 1 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {ctp 4157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-un 3565  df-sn 4154  df-pr 4156  df-tp 4158
This theorem is referenced by:  fz0tp  12378  fz0to4untppr  12380  fzo0to3tp  12492  fzo1to4tp  12494  prdsval  16031  imasval  16087  fucval  16534  fucpropd  16553  setcval  16643  catcval  16662  estrcval  16680  xpcval  16733  symgval  17715  psrval  19276  om1val  22733  ldualset  33878  erngfset  35553  erngfset-rN  35561  dvafset  35758  dvaset  35759  dvhfset  35835  dvhset  35836  hlhilset  36692  rabren3dioph  36845  mendval  37220  nnsum4primesodd  40961  nnsum4primesoddALTV  40962  rngcvalALTV  41222  ringcvalALTV  41268
  Copyright terms: Public domain W3C validator