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 2768 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtri.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtr2i 2769 | 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 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-9 2120 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1787 df-cleq 2732 |
This theorem is referenced by: dfif5 4481 resindm 5938 difxp1 6066 difxp2 6067 dfdm2 6182 cofunex2g 7780 df1st2 7923 df2nd2 7924 domss2 8897 adderpqlem 10703 dfn2 12238 9p1e10 12430 sqrtm1 14977 0.999... 15583 pockthi 16598 matgsum 21576 indistps 22151 indistps2 22152 refun0 22656 filconn 23024 sincosq3sgn 25647 sincosq4sgn 25648 eff1o 25695 ax5seglem7 27293 0grsubgr 27635 nbupgrres 27721 vtxdginducedm1fi 27901 clwwlknclwwlkdif 28331 cnnvg 29028 cnnvs 29030 cnnvnm 29031 h2hva 29324 h2hsm 29325 h2hnm 29326 hhssva 29607 hhsssm 29608 hhssnm 29609 spansnji 29996 lnopunilem1 30360 lnophmlem2 30367 stadd3i 30598 indifundif 30861 dpmul4 31176 xrsp0 31278 xrsp1 31279 hgt750lemd 32616 hgt750lem 32619 rankeq1o 34461 poimirlem8 35773 mbfposadd 35812 iocunico 41031 corcltrcl 41309 binomcxplemdvsum 41935 cosnegpi 43371 fourierdlem62 43672 fouriersw 43735 salexct3 43844 salgensscntex 43846 caragenuncllem 44013 isomenndlem 44031 |
Copyright terms: Public domain | W3C validator |