Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtrrd | Unicode version |
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof 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 2150 | . 2 |
4 | 3eqtrd.3 | . 2 | |
5 | 3, 4 | eqtr2d 2151 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: nnanq0 7234 1idprl 7366 1idpru 7367 axcnre 7657 fseq1p1m1 9842 expmulzap 10307 expubnd 10318 subsq 10367 bcm1k 10474 bcpasc 10480 crim 10598 rereb 10603 fsumparts 11207 isumshft 11227 geosergap 11243 efsub 11314 sincossq 11382 efieq1re 11405 bezoutlema 11614 bezoutlemb 11615 eucalg 11667 phiprmpw 11825 strsetsid 11919 setsslid 11936 upxp 12368 uptx 12370 |
Copyright terms: Public domain | W3C validator |