![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3eqtr2i | Structured version Visualization version Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) |
Ref | Expression |
---|---|
3eqtr2i.1 |
![]() ![]() ![]() ![]() |
3eqtr2i.2 |
![]() ![]() ![]() ![]() |
3eqtr2i.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr2i |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr2i.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 3eqtr2i.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtr4i 2487 |
. 2
![]() ![]() ![]() ![]() |
4 | 3eqtr2i.3 |
. 2
![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtri 2484 |
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 1680 ax-4 1693 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-cleq 2455 |
This theorem is referenced by: indif 3697 dfrab3 3730 iunid 4347 cnvcnv 5307 cocnvcnv2 5366 fmptap 6111 fpar 6927 fodomr 7749 jech9.3 8311 cda1dif 8632 alephadd 9028 distrnq 9412 ltanq 9422 ltrnq 9430 negdiiOLD 9985 halfpm6th 10863 numma 11111 numaddc 11115 6p5lem 11129 binom2i 12416 faclbnd4lem1 12510 0.999... 13986 6gcd4e2 14551 dfphi2 14771 mod2xnegi 15092 karatsuba 15105 1259lem1 15151 oppgtopn 17053 mgptopn 17781 ply1plusg 18867 ply1vsca 18868 ply1mulr 18869 restcld 20237 cmpsublem 20463 kgentopon 20602 txswaphmeolem 20868 dfii5 21966 itg1climres 22721 ang180lem1 23787 1cubrlem 23816 quart1lem 23830 efiatan 23887 log2cnv 23919 1sgm2ppw 24177 ppiub 24181 bposlem8 24268 bposlem9 24269 ax5seglem7 25014 usgraexmplcvtx 25182 usgraexmplcedg 25183 ipidsq 26398 ipdirilem 26519 norm3difi 26849 polid2i 26859 pjclem3 27899 cvmdi 28026 indifundif 28201 eulerpartlemt 29253 eulerpart 29264 ballotlem1 29368 ballotlemfval0 29377 ballotth 29419 ballotthOLD 29457 subfaclim 29960 kur14lem6 29983 quad3 30351 iexpire 30420 pigt3 31983 volsupnfl 32030 areaquad 36146 wallispilem4 37968 dirkertrigeqlem3 38000 dirkercncflem1 38003 fourierswlem 38132 fouriersw 38133 tgoldbachlt 38947 3exp4mod41 38954 41prothprm 38957 2pthd 39889 3pthd 39915 zlmodzxz0 40410 linevalexample 40461 |
Copyright terms: Public domain | W3C validator |