![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3eqtrri | Structured version Visualization version GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtri.1 | ⊢ 𝐴 = 𝐵 |
3eqtri.2 | ⊢ 𝐵 = 𝐶 |
3eqtri.3 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
3eqtrri | ⊢ 𝐷 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtri.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 3eqtri.2 | . . 3 ⊢ 𝐵 = 𝐶 | |
3 | 1, 2 | eqtri 2756 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtri.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtr2i 2757 | 1 ⊢ 𝐷 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-cleq 2720 |
This theorem is referenced by: dfif5 4540 resindm 6028 difxp1 6163 difxp2 6164 dfdm2 6279 cofunex2g 7947 df1st2 8097 df2nd2 8098 domss2 9154 adderpqlem 10971 dfn2 12509 9p1e10 12703 sqrtm1 15248 0.999... 15853 pockthi 16869 matgsum 22332 indistps 22907 indistps2 22908 refun0 23412 filconn 23780 sincosq3sgn 26428 sincosq4sgn 26429 eff1o 26476 ax5seglem7 28739 0grsubgr 29084 nbupgrres 29170 vtxdginducedm1fi 29351 clwwlknclwwlkdif 29782 cnnvg 30481 cnnvs 30483 cnnvnm 30484 h2hva 30777 h2hsm 30778 h2hnm 30779 hhssva 31060 hhsssm 31061 hhssnm 31062 spansnji 31449 lnopunilem1 31813 lnophmlem2 31820 stadd3i 32051 indifundif 32314 dpmul4 32631 xrsp0 32733 xrsp1 32734 hgt750lemd 34274 hgt750lem 34277 rankeq1o 35761 poimirlem8 37095 mbfposadd 37134 iocunico 42633 corcltrcl 43163 binomcxplemdvsum 43786 cosnegpi 45249 fourierdlem62 45550 fouriersw 45613 salexct3 45724 salgensscntex 45726 caragenuncllem 45894 isomenndlem 45912 |
Copyright terms: Public domain | W3C validator |