![]() |
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 2756 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtr2i.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtri 2753 | 1 ⊢ 𝐴 = 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 |
This theorem is referenced by: indif 4268 dfrab3 4308 iunidOLD 5065 cocnvcnv2 6264 fmptap 7179 cnvoprab 8065 fpar 8121 fodomr 9153 jech9.3 9839 dju1dif 10197 alephadd 10602 distrnq 10986 ltanq 10996 ltrnq 11004 1p2e3 12388 halfpm6th 12466 numma 12754 numaddc 12758 6p5lem 12780 8p2e10 12790 binom2i 14211 faclbnd4lem1 14288 cats2cat 14849 0.999... 15863 flodddiv4 16393 6gcd4e2 16517 dfphi2 16746 mod2xnegi 17043 karatsuba 17056 1259lem1 17103 setc2obas 18086 oppgtopn 19319 symgplusg 19349 cmnbascntr 19772 mgptopn 20098 ply1plusg 22166 ply1vsca 22167 ply1mulr 22168 restcld 23120 cmpsublem 23347 kgentopon 23486 dfii5 24849 itg1climres 25688 pigt3 26497 ang180lem1 26786 1cubrlem 26818 quart1lem 26832 efiatan 26889 log2cnv 26921 log2ublem3 26925 1sgm2ppw 27178 ppiub 27182 bposlem8 27269 bposlem9 27270 2lgsoddprmlem3c 27390 2lgsoddprmlem3d 27391 bday1s 27810 addsasslem2 27967 seqsval 28211 ax5seglem7 28818 wlknwwlksnbij 29771 2pthd 29823 3pthd 30056 ipidsq 30592 ipdirilem 30711 norm3difi 31029 polid2i 31039 pjclem3 32079 cvmdi 32206 indifundif 32400 dpmul 32721 tocyccntz 32957 ccfldextdgrr 33491 eulerpartlemt 34122 eulerpart 34133 ballotlem1 34237 ballotlemfval0 34246 ballotth 34288 hgt750lem 34414 hgt750lem2 34415 subfaclim 34929 kur14lem6 34952 quad3 35405 iexpire 35460 volsupnfl 37269 dfxrn2 37978 xrninxp 37994 ipiiie0 42127 sn-0tie0 42129 areaquad 42786 wallispilem4 45594 dirkertrigeqlem3 45626 dirkercncflem1 45629 fourierswlem 45756 fouriersw 45757 smflimsuplem8 46353 3exp4mod41 47093 41prothprm 47096 tgoldbachlt 47293 zlmodzxz0 47606 linevalexample 47649 mndtcco 48283 |
Copyright terms: Public domain | W3C validator |