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 2647 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtr2i.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtri 2644 | 1 ⊢ 𝐴 = 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 |
This theorem is referenced by: indif 3869 dfrab3 3902 iunid 4575 cnvcnvOLD 5587 cocnvcnv2 5647 fmptap 6436 fpar 7281 fodomr 8111 jech9.3 8677 cda1dif 8998 alephadd 9399 distrnq 9783 ltanq 9793 ltrnq 9801 halfpm6th 11253 numma 11557 numaddc 11561 6p5lem 11595 8p2e10 11610 binom2i 12974 faclbnd4lem1 13080 cats2cat 13607 0.999... 14612 0.999...OLD 14613 flodddiv4 15137 6gcd4e2 15255 dfphi2 15479 mod2xnegi 15775 karatsuba 15792 karatsubaOLD 15793 1259lem1 15838 oppgtopn 17783 mgptopn 18498 ply1plusg 19595 ply1vsca 19596 ply1mulr 19597 restcld 20976 cmpsublem 21202 kgentopon 21341 txswaphmeolem 21607 dfii5 22688 itg1climres 23481 ang180lem1 24539 1cubrlem 24568 quart1lem 24582 efiatan 24639 log2cnv 24671 log2ublem3 24675 1sgm2ppw 24925 ppiub 24929 bposlem8 25016 bposlem9 25017 2lgsoddprmlem3c 25137 2lgsoddprmlem3d 25138 ax5seglem7 25815 2pthd 26836 3pthd 27034 ipidsq 27565 ipdirilem 27684 norm3difi 28004 polid2i 28014 pjclem3 29056 cvmdi 29183 indifundif 29356 dpmul 29621 eulerpartlemt 30433 eulerpart 30444 ballotlem1 30548 ballotlemfval0 30557 ballotth 30599 hgt750lem 30729 hgt750lem2 30730 subfaclim 31170 kur14lem6 31193 quad3 31564 iexpire 31621 pigt3 33402 volsupnfl 33454 areaquad 37802 wallispilem4 40285 dirkertrigeqlem3 40317 dirkercncflem1 40320 fourierswlem 40447 fouriersw 40448 smflimsuplem8 41033 3exp4mod41 41533 41prothprm 41536 tgoldbachlt 41704 tgoldbachltOLD 41710 zlmodzxz0 42134 linevalexample 42184 |
Copyright terms: Public domain | W3C validator |