![]() |
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 4066 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | tpeq123d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | tpeq2d 4067 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | tpeq123d.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | tpeq3d 4068 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 4, 6 | 3eqtrd 2491 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-v 3049 df-un 3411 df-sn 3971 df-pr 3973 df-tp 3975 |
This theorem is referenced by: fz0tp 11900 fzo0to3tp 12006 prdsval 15365 imasval 15423 imasvalOLD 15424 fucval 15875 fucpropd 15894 setcval 15984 catcval 16003 estrcval 16021 xpcval 16074 symgval 17032 psrval 18598 om1val 22073 usgraexmplvtxlem 25134 ldualset 32703 erngfset 34378 erngfset-rN 34386 dvafset 34583 dvaset 34584 dvhfset 34660 dvhset 34661 hlhilset 35517 rabren3dioph 35670 mendval 36061 nnsum4primesodd 38901 nnsum4primesoddALTV 38902 rngcvalALTV 40067 ringcvalALTV 40113 |
Copyright terms: Public domain | W3C validator |