![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3eqtr2i | Structured version Visualization version GIF 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 2773 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtr2i.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtri 2770 | 1 ⊢ 𝐴 = 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1620 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1842 df-cleq 2741 |
This theorem is referenced by: indif 4000 dfrab3 4033 iunid 4715 cnvcnvOLD 5733 cocnvcnv2 5796 fmptap 6588 cnvoprab 7385 fpar 7437 fodomr 8264 jech9.3 8838 cda1dif 9161 alephadd 9562 distrnq 9946 ltanq 9956 ltrnq 9964 halfpm6th 11416 numma 11720 numaddc 11724 6p5lem 11758 8p2e10 11773 binom2i 13139 faclbnd4lem1 13245 cats2cat 13778 0.999... 14782 0.999...OLD 14783 flodddiv4 15310 6gcd4e2 15428 dfphi2 15652 mod2xnegi 15948 karatsuba 15965 karatsubaOLD 15966 1259lem1 16011 oppgtopn 17954 mgptopn 18669 ply1plusg 19768 ply1vsca 19769 ply1mulr 19770 restcld 21149 cmpsublem 21375 kgentopon 21514 txswaphmeolem 21780 dfii5 22860 itg1climres 23651 ang180lem1 24709 1cubrlem 24738 quart1lem 24752 efiatan 24809 log2cnv 24841 log2ublem3 24845 1sgm2ppw 25095 ppiub 25099 bposlem8 25186 bposlem9 25187 2lgsoddprmlem3c 25307 2lgsoddprmlem3d 25308 ax5seglem7 25985 2pthd 27031 3pthd 27297 ipidsq 27845 ipdirilem 27964 norm3difi 28284 polid2i 28294 pjclem3 29336 cvmdi 29463 indifundif 29634 dpmul 29901 eulerpartlemt 30713 eulerpart 30724 ballotlem1 30828 ballotlemfval0 30837 ballotth 30879 hgt750lem 31009 hgt750lem2 31010 subfaclim 31448 kur14lem6 31471 quad3 31842 iexpire 31899 pigt3 33684 volsupnfl 33736 dfxrn2 34430 xrninxp 34442 areaquad 38273 wallispilem4 40757 dirkertrigeqlem3 40789 dirkercncflem1 40792 fourierswlem 40919 fouriersw 40920 smflimsuplem8 41508 3exp4mod41 42012 41prothprm 42015 tgoldbachlt 42183 tgoldbachltOLD 42189 zlmodzxz0 42613 linevalexample 42663 |
Copyright terms: Public domain | W3C validator |