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

Theorem tpeq123d 4417
 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 4414 . 2 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3 tpeq123d.2 . . 3 (𝜑𝐶 = 𝐷)
43tpeq2d 4415 . 2 (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5 tpeq123d.3 . . 3 (𝜑𝐸 = 𝐹)
65tpeq3d 4416 . 2 (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
72, 4, 63eqtrd 2808 1 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1630  {ctp 4318 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726  df-sn 4315  df-pr 4317  df-tp 4319 This theorem is referenced by:  fz0tp  12647  fz0to4untppr  12649  fzo0to3tp  12761  fzo1to4tp  12763  prdsval  16322  imasval  16378  fucval  16824  fucpropd  16843  setcval  16933  catcval  16952  estrcval  16970  xpcval  17024  symgval  18005  psrval  19576  om1val  23048  ldualset  34927  erngfset  36601  erngfset-rN  36609  dvafset  36806  dvaset  36807  dvhfset  36883  dvhset  36884  hlhilset  37737  rabren3dioph  37898  mendval  38272  nnsum4primesodd  42202  nnsum4primesoddALTV  42203  rngcvalALTV  42479  ringcvalALTV  42525
 Copyright terms: Public domain W3C validator