Theorem tpeq123d 4684

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

Syntax hints:   → wi 4   = wceq 1539  {ctp 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564  df-tp 4566

This theorem is referenced by:  fz0tp  13357  fz0to4untppr  13359  fzo0to3tp  13473  fzo1to4tp  13475  prdsval  17166  imasval  17222  fucval  17675  fucpropd  17695  setcval  17792  catcval  17815  estrcval  17840  xpcval  17894  efmnd  18509  psrval  21118  om1val  24193  s3rn  31220  idlsrgval  31648  ldualset  37139  erngfset  38813  erngfset-rN  38821  dvafset  39018  dvaset  39019  dvhfset  39094  dvhset  39095  hlhilset  39948  rabren3dioph  40637  mendval  41008  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  rngcvalALTV  45519  ringcvalALTV  45565  mndtcval  46366