| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: A deduction from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Ref | Expression |
|---|---|
| 3eqtrd.1 |
|
| 3eqtrd.2 |
|
| 3eqtrd.3 |
|
| Ref | Expression |
|---|---|
| 3eqtrrd |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3eqtrd.1 |
. . 3
| |
| 2 | 3eqtrd.2 |
. . 3
| |
| 3 | 1, 2 | eqtrd 1925 |
. 2
|
| 4 | 3eqtrd.3 |
. 2
| |
| 5 | 3, 4 | eqtr2d 1926 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: axcnre 6439 seq1seq02 7786 seqzp1 7791 expubnd 7853 subsq 7888 rereb 8026 sincossq 8726 efieq1re 8751 abssinper 10062 upxp 10225 nmbdoplbi 11586 nmcopexlem3 11590 nmcoplbi 11595 nmbdfnlbi 11615 nmcfnexlem3 11619 nmcfnlbi 11624 hstoh 11804 eucalg 13755 fprodneg 14741 ismrer1 16024 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1305 ax-17 1317 ax-4 1319 ax-5o 1321 ax-ext 1865 |
| This theorem depends on definitions: df-bi 164 df-an 242 df-cleq 1877 |