![]() |
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 2802 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtri.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtr2i 2803 | 1 ⊢ 𝐷 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2771 |
This theorem is referenced by: dfif5 4367 resindm 5747 difxp1 5864 difxp2 5865 dfdm2 5972 cofunex2g 7465 df1st2 7603 df2nd2 7604 domss2 8474 adderpqlem 10176 dfn2 11725 9p1e10 11916 sqrtm1 14499 0.999... 15100 pockthi 16102 matgsum 20753 indistps 21326 indistps2 21327 refun0 21830 filconn 22198 sincosq3sgn 24792 sincosq4sgn 24793 eff1o 24837 ax5seglem7 26427 0grsubgr 26766 nbupgrres 26852 vtxdginducedm1fi 27032 clwwlknclwwlkdif 27488 cnnvg 28235 cnnvs 28237 cnnvnm 28238 h2hva 28533 h2hsm 28534 h2hnm 28535 hhssva 28816 hhsssm 28817 hhssnm 28818 spansnji 29207 lnopunilem1 29571 lnophmlem2 29578 stadd3i 29809 indifundif 30062 dpmul4 30339 xrsp0 30400 xrsp1 30401 hgt750lemd 31567 hgt750lem 31570 rankeq1o 33153 poimirlem8 34341 mbfposadd 34380 iocunico 39213 corcltrcl 39447 binomcxplemdvsum 40103 cosnegpi 41579 fourierdlem62 41885 fouriersw 41948 salexct3 42057 salgensscntex 42059 caragenuncllem 42226 isomenndlem 42244 |
Copyright terms: Public domain | W3C validator |