Theorem tpeq123d 4701

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

Syntax hints:   → wi 4   = wceq 1541  {ctp 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579  df-tp 4581

This theorem is referenced by:  fz0tp  13528  fz0to5un2tp  13531  fzo0to3tp  13652  fzo1to4tp  13654  prdsval  17359  imasval  17415  fucval  17868  fucpropd  17887  setcval  17984  catcval  18007  estrcval  18030  xpcval  18083  efmnd  18778  dfcnfldOLD  21308  psrval  21853  om1val  24958  s3rnOLD  32925  rlocval  33224  idlsrgval  33466  ldualset  39170  erngfset  40844  erngfset-rN  40852  dvafset  41049  dvaset  41050  dvhfset  41125  dvhset  41126  hlhilset  41979  rabren3dioph  42854  mendval  43218  oaun3  43421  nnsum4primesodd  47833  nnsum4primesoddALTV  47834  rngcvalALTV  48302  ringcvalALTV  48326  mndtcval  49617