![]() |
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 2761 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtri.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtr2i 2762 | 1 ⊢ 𝐷 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 |
This theorem is referenced by: dfif5 4506 resindm 5990 difxp1 6121 difxp2 6122 dfdm2 6237 cofunex2g 7886 df1st2 8034 df2nd2 8035 domss2 9086 adderpqlem 10898 dfn2 12434 9p1e10 12628 sqrtm1 15169 0.999... 15774 pockthi 16787 matgsum 21809 indistps 22384 indistps2 22385 refun0 22889 filconn 23257 sincosq3sgn 25880 sincosq4sgn 25881 eff1o 25928 ax5seglem7 27933 0grsubgr 28275 nbupgrres 28361 vtxdginducedm1fi 28541 clwwlknclwwlkdif 28972 cnnvg 29669 cnnvs 29671 cnnvnm 29672 h2hva 29965 h2hsm 29966 h2hnm 29967 hhssva 30248 hhsssm 30249 hhssnm 30250 spansnji 30637 lnopunilem1 31001 lnophmlem2 31008 stadd3i 31239 indifundif 31502 dpmul4 31826 xrsp0 31928 xrsp1 31929 hgt750lemd 33325 hgt750lem 33328 rankeq1o 34809 poimirlem8 36136 mbfposadd 36175 iocunico 41592 corcltrcl 42103 binomcxplemdvsum 42727 cosnegpi 44198 fourierdlem62 44499 fouriersw 44562 salexct3 44673 salgensscntex 44675 caragenuncllem 44843 isomenndlem 44861 |
Copyright terms: Public domain | W3C validator |