Theorem tpeq123d 4644

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

Syntax hints:   → wi 4   = wceq 1538  {ctp 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-tp 4530

This theorem is referenced by:  fz0tp  13003  fz0to4untppr  13005  fzo0to3tp  13118  fzo1to4tp  13120  prdsval  16720  imasval  16776  fucval  17220  fucpropd  17239  setcval  17329  catcval  17348  estrcval  17366  xpcval  17419  efmnd  18027  psrval  20600  om1val  23635  s3rn  30648  idlsrgval  31056  ldualset  36421  erngfset  38095  erngfset-rN  38103  dvafset  38300  dvaset  38301  dvhfset  38376  dvhset  38377  hlhilset  39230  rabren3dioph  39756  mendval  40127  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  rngcvalALTV  44585  ringcvalALTV  44631