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

Theorem tpeq123d 4751
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 4748 . 2 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3 tpeq123d.2 . . 3 (𝜑𝐶 = 𝐷)
43tpeq2d 4749 . 2 (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5 tpeq123d.3 . . 3 (𝜑𝐸 = 𝐹)
65tpeq3d 4750 . 2 (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
72, 4, 63eqtrd 2774 1 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  {ctp 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952  df-sn 4628  df-pr 4630  df-tp 4632
This theorem is referenced by:  fz0tp  13606  fz0to4untppr  13608  fzo0to3tp  13722  fzo1to4tp  13724  prdsval  17405  imasval  17461  fucval  17914  fucpropd  17934  setcval  18031  catcval  18054  estrcval  18079  xpcval  18133  efmnd  18787  psrval  21687  om1val  24777  s3rn  32379  idlsrgval  32891  gg-dfcnfld  35473  ldualset  38298  erngfset  39973  erngfset-rN  39981  dvafset  40178  dvaset  40179  dvhfset  40254  dvhset  40255  hlhilset  41108  rabren3dioph  41855  mendval  42227  oaun3  42434  nnsum4primesodd  46762  nnsum4primesoddALTV  46763  rngcvalALTV  46947  ringcvalALTV  46993  mndtcval  47792
  Copyright terms: Public domain W3C validator