Theorem tpeq123d 4712

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

Step	Hyp	Ref	Expression
1		tpeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	tpeq1d 4709	. 2 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3		tpeq123d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	tpeq2d 4710	. 2 ⊢ (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5		tpeq123d.3	. . 3 ⊢ (𝜑 → 𝐸 = 𝐹)
6	5	tpeq3d 4711	. 2 ⊢ (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
7	2, 4, 6	3eqtrd 2801	1 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {ctp 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590  df-tp 4592

This theorem is used by:  fz0tp  13687  fz0to5un2tp  13690  fzo0to3tp  13812  fzo1to4tp  13814  prdsval  17546  imasval  17603  fucval  18056  fucpropd  18075  setcval  18172  catcval  18195  estrcval  18218  xpcval  18271  efmnd  18985  psrval  22136  om1val  25264  angmgmval  29281  rlocval  33707  idlsrgval  33921  ldualset  40006  erngfset  41680  erngfset-rN  41688  dvafset  41885  dvaset  41886  dvhfset  41961  dvhset  41962  hlhilset  42815  rabren3dioph  43664  mendval  44028  oaun3  44231  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  rngcvalALTV  49188  ringcvalALTV  49212  mndtcval  50513  crosspdotsumlem  50805