![]() |
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 2807 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtr2i.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtri 2804 | 1 ⊢ 𝐴 = 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1508 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-9 2060 ax-ext 2752 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-cleq 2773 |
This theorem is referenced by: indif 4136 dfrab3 4168 iunid 4855 cocnvcnv2 5955 fmptap 6761 cnvoprab 7572 fpar 7625 fodomr 8470 jech9.3 9043 dju1dif 9402 alephadd 9803 distrnq 10187 ltanq 10197 ltrnq 10205 1p2e3 11596 halfpm6th 11674 numma 11962 numaddc 11966 6p5lem 11989 8p2e10 11999 binom2i 13395 faclbnd4lem1 13474 cats2cat 14092 0.999... 15103 flodddiv4 15630 6gcd4e2 15748 dfphi2 15973 mod2xnegi 16269 karatsuba 16282 1259lem1 16326 oppgtopn 18264 mgptopn 18983 ply1plusg 20111 ply1vsca 20112 ply1mulr 20113 restcld 21499 cmpsublem 21726 kgentopon 21865 txswaphmeolem 22131 dfii5 23211 itg1climres 24033 pigt3 24821 ang180lem1 25103 1cubrlem 25135 quart1lem 25149 efiatan 25206 log2cnv 25239 log2ublem3 25243 1sgm2ppw 25493 ppiub 25497 bposlem8 25584 bposlem9 25585 2lgsoddprmlem3c 25705 2lgsoddprmlem3d 25706 ax5seglem7 26439 wlknwwlksnbij 27390 2pthd 27461 3pthd 27718 ipidsq 28279 ipdirilem 28398 norm3difi 28718 polid2i 28728 pjclem3 29770 cvmdi 29897 indifundif 30074 dpmul 30359 ccfldextdgrr 30718 eulerpartlemt 31306 eulerpart 31317 ballotlem1 31422 ballotlemfval0 31431 ballotth 31473 hgt750lem 31602 hgt750lem2 31603 subfaclim 32060 kur14lem6 32083 quad3 32473 iexpire 32527 volsupnfl 34418 dfxrn2 35113 xrninxp 35125 areaquad 39260 wallispilem4 41819 dirkertrigeqlem3 41851 dirkercncflem1 41854 fourierswlem 41981 fouriersw 41982 smflimsuplem8 42567 3exp4mod41 43184 41prothprm 43187 tgoldbachlt 43384 zlmodzxz0 43803 linevalexample 43852 |
Copyright terms: Public domain | W3C validator |