|   | 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 2767 | . 2 ⊢ 𝐴 = 𝐶 | 
| 4 | 3eqtr2i.3 | . 2 ⊢ 𝐶 = 𝐷 | |
| 5 | 3, 4 | eqtri 2764 | 1 ⊢ 𝐴 = 𝐷 | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 | 
| This theorem is referenced by: indif 4279 dfrab3 4318 iunidOLD 5060 cocnvcnv2 6277 fmptap 7191 cnvoprab 8086 fpar 8142 fodomr 9169 fodomfir 9369 jech9.3 9855 dju1dif 10214 alephadd 10618 distrnq 11002 ltanq 11012 ltrnq 11020 1p2e3 12410 halfpm6th 12490 numma 12779 numaddc 12783 6p5lem 12805 8p2e10 12815 binom2i 14252 faclbnd4lem1 14333 cats2cat 14902 0.999... 15918 flodddiv4 16453 6gcd4e2 16576 dfphi2 16812 mod2xnegi 17110 karatsuba 17122 1259lem1 17169 setc2obas 18140 oppgtopn 19373 symgplusg 19401 cmnbascntr 19824 mgptopn 20146 ply1plusg 22226 ply1vsca 22227 ply1mulr 22228 restcld 23181 cmpsublem 23408 kgentopon 23547 dfii5 24912 itg1climres 25750 pigt3 26561 ang180lem1 26853 1cubrlem 26885 quart1lem 26899 efiatan 26956 log2cnv 26988 log2ublem3 26992 1sgm2ppw 27245 ppiub 27249 bposlem8 27336 bposlem9 27337 2lgsoddprmlem3c 27457 2lgsoddprmlem3d 27458 bday1s 27877 addsasslem2 28038 seqsval 28295 pw2bday 28419 ax5seglem7 28951 wlknwwlksnbij 29909 2pthd 29961 3pthd 30194 ipidsq 30730 ipdirilem 30849 norm3difi 31167 polid2i 31177 pjclem3 32217 cvmdi 32344 indifundif 32544 dpmul 32896 tocyccntz 33165 ccfldextdgrr 33723 eulerpartlemt 34374 eulerpart 34385 ballotlem1 34490 ballotlemfval0 34499 ballotth 34541 hgt750lem 34667 hgt750lem2 34668 subfaclim 35194 kur14lem6 35217 quad3 35676 iexpire 35736 volsupnfl 37673 dfxrn2 38378 xrninxp 38394 ipiiie0 42472 sn-0tie0 42474 areaquad 43233 wallispilem4 46088 dirkertrigeqlem3 46120 dirkercncflem1 46123 fourierswlem 46250 fouriersw 46251 smflimsuplem8 46847 ceil5half3 47347 3exp4mod41 47608 41prothprm 47611 tgoldbachlt 47808 zlmodzxz0 48277 linevalexample 48317 mndtcco 49237 | 
| Copyright terms: Public domain | W3C validator |