Theorem tpeq123d 4760

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

Syntax hints:   → wi 4   = wceq 1534  {ctp 4640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-un 3964  df-sn 4637  df-pr 4639  df-tp 4641

This theorem is referenced by:  fz0tp  13666  fz0to4untppr  13668  fzo0to3tp  13782  fzo1to4tp  13784  prdsval  17491  imasval  17547  fucval  18003  fucpropd  18023  setcval  18120  catcval  18143  estrcval  18168  xpcval  18222  efmnd  18881  dfcnfldOLD  21381  psrval  21934  om1val  25071  s3rn  32837  rlocval  33144  idlsrgval  33409  ldualset  38870  erngfset  40545  erngfset-rN  40553  dvafset  40750  dvaset  40751  dvhfset  40826  dvhset  40827  hlhilset  41680  rabren3dioph  42543  mendval  42915  oaun3  43119  nnsum4primesodd  47438  nnsum4primesoddALTV  47439  rngcvalALTV  47723  ringcvalALTV  47747  mndtcval  48487