Theorem tpeq123d 4124

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 4121	. 2
3		tpeq123d.2	. . 3
4	3	tpeq2d 4122	. 2
5		tpeq123d.3	. . 3
6	5	tpeq3d 4123	. 2
7	2, 4, 6	3eqtrd 2502	1

Syntax hints:  ->wi 4  =wceq 1395  {ctp 4033

This theorem is referenced by:  fz0tp  11806  fzo0to3tp  11900  prdsval  14852  imasval  14908  fucval  15327  fucpropd  15346  setcval  15404  catcval  15423  xpcval  15446  symgval  16404  psrval  18011  om1val  21530  usgraexvlem  24395  rabren3dioph  30749  mendval  31132  estrcval  32630  rngcvalOLD  32769  ringcvalOLD  32815  ldualset  34850  erngfset  36525  erngfset-rN  36533  dvafset  36730  dvaset  36731  dvhfset  36807  dvhset  36808  hlhilset  37664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032  df-tp 4034