Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > tpeq123d | Structured version Visualization version Unicode version |
Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
Ref | Expression |
---|---|
tpeq1d.1 | |
tpeq123d.2 | |
tpeq123d.3 |
Ref | Expression |
---|---|
tpeq123d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tpeq1d.1 | . . 3 | |
2 | 1 | tpeq1d 4280 | . 2 |
3 | tpeq123d.2 | . . 3 | |
4 | 3 | tpeq2d 4281 | . 2 |
5 | tpeq123d.3 | . . 3 | |
6 | 5 | tpeq3d 4282 | . 2 |
7 | 2, 4, 6 | 3eqtrd 2660 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 ctp 4181 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 df-sn 4178 df-pr 4180 df-tp 4182 |
This theorem is referenced by: fz0tp 12440 fz0to4untppr 12442 fzo0to3tp 12554 fzo1to4tp 12556 prdsval 16115 imasval 16171 fucval 16618 fucpropd 16637 setcval 16727 catcval 16746 estrcval 16764 xpcval 16817 symgval 17799 psrval 19362 om1val 22830 ldualset 34412 erngfset 36087 erngfset-rN 36095 dvafset 36292 dvaset 36293 dvhfset 36369 dvhset 36370 hlhilset 37226 rabren3dioph 37379 mendval 37753 nnsum4primesodd 41684 nnsum4primesoddALTV 41685 rngcvalALTV 41961 ringcvalALTV 42007 |
Copyright terms: Public domain | W3C validator |