Theorem tpeq123d 4708

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 4705	. 2 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3		tpeq123d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	tpeq2d 4706	. 2 ⊢ (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5		tpeq123d.3	. . 3 ⊢ (𝜑 → 𝐸 = 𝐹)
6	5	tpeq3d 4707	. 2 ⊢ (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
7	2, 4, 6	3eqtrd 2799	1 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {ctp 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3901  df-sn 4584  df-pr 4586  df-tp 4588

This theorem is used by:  fz0tp  13762  fz0to5un2tp  13765  fzo0to3tp  13887  fzo1to4tp  13889  prdsval  17626  imasval  17683  fucval  18136  fucpropd  18155  setcval  18252  catcval  18275  estrcval  18298  xpcval  18351  efmnd  19066  psrval  22223  om1val  25351  angmgmval  29394  rlocval  33820  idlsrgval  34035  ldualset  40183  erngfset  41857  erngfset-rN  41865  dvafset  42062  dvaset  42063  dvhfset  42138  dvhset  42139  hlhilset  42992  rabren3dioph  43822  mendval  44181  oaun3  44384  nnsum4primesodd  48894  nnsum4primesoddALTV  48895  rngcvalALTV  49362  ringcvalALTV  49386  mndtcval  50687  crosspdotsumlem  50964