MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tpeq123d Unicode version

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
StepHypRef Expression
1 tpeq1d.1 . . 3
21tpeq1d 4121 . 2
3 tpeq123d.2 . . 3
43tpeq2d 4122 . 2
5 tpeq123d.3 . . 3
65tpeq3d 4123 . 2
72, 4, 63eqtrd 2502 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator