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 2768 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtr2i.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtri 2765 | 1 ⊢ 𝐴 = 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-cleq 2729 |
This theorem is referenced by: indif 4181 dfrab3 4221 iunid 4966 cocnvcnv2 6119 fmptap 6982 cnvoprab 7827 fpar 7881 fodomr 8794 jech9.3 9427 dju1dif 9783 alephadd 10188 distrnq 10572 ltanq 10582 ltrnq 10590 1p2e3 11970 halfpm6th 12048 numma 12334 numaddc 12338 6p5lem 12360 8p2e10 12370 binom2i 13777 faclbnd4lem1 13856 cats2cat 14424 0.999... 15442 flodddiv4 15971 6gcd4e2 16095 dfphi2 16324 mod2xnegi 16621 karatsuba 16634 1259lem1 16681 setc2obas 17597 oppgtopn 18742 symgplusg 18772 mgptopn 19510 ply1plusg 21143 ply1vsca 21144 ply1mulr 21145 restcld 22066 cmpsublem 22293 kgentopon 22432 dfii5 23779 itg1climres 24609 pigt3 25404 ang180lem1 25689 1cubrlem 25721 quart1lem 25735 efiatan 25792 log2cnv 25824 log2ublem3 25828 1sgm2ppw 26078 ppiub 26082 bposlem8 26169 bposlem9 26170 2lgsoddprmlem3c 26290 2lgsoddprmlem3d 26291 ax5seglem7 27023 wlknwwlksnbij 27969 2pthd 28021 3pthd 28254 ipidsq 28788 ipdirilem 28907 norm3difi 29225 polid2i 29235 pjclem3 30275 cvmdi 30402 indifundif 30589 dpmul 30904 tocyccntz 31127 ccfldextdgrr 31453 eulerpartlemt 32047 eulerpart 32058 ballotlem1 32162 ballotlemfval0 32171 ballotth 32213 hgt750lem 32340 hgt750lem2 32341 subfaclim 32860 kur14lem6 32883 quad3 33338 iexpire 33416 bday1s 33759 volsupnfl 35557 dfxrn2 36241 xrninxp 36253 ipiiie0 40125 sn-0tie0 40127 areaquad 40748 wallispilem4 43282 dirkertrigeqlem3 43314 dirkercncflem1 43317 fourierswlem 43444 fouriersw 43445 smflimsuplem8 44030 3exp4mod41 44739 41prothprm 44742 tgoldbachlt 44939 zlmodzxz0 45363 linevalexample 45407 mndtcco 46041 |
Copyright terms: Public domain | W3C validator |