![]() |
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 2673 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtri.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtr2i 2674 | 1 ⊢ 𝐷 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 |
This theorem is referenced by: dfif5 4135 resindm 5479 difxp1 5594 difxp2 5595 dfdm2 5705 cofunex2g 7173 df1st2 7308 df2nd2 7309 domss2 8160 adderpqlem 9814 dfn2 11343 9p1e10 11534 sq10OLD 13091 sqrtm1 14060 0.999... 14656 0.999...OLD 14657 pockthi 15658 matgsum 20291 indistps 20863 indistps2 20864 refun0 21366 filconn 21734 sincosq3sgn 24297 sincosq4sgn 24298 eff1o 24340 ax5seglem7 25860 0grsubgr 26215 nbupgrres 26310 vtxdginducedm1fi 26496 clwwlknclwwlkdif 26945 clwwlknclwwlkdifsOLD 26947 cnnvg 27661 cnnvs 27663 cnnvnm 27664 h2hva 27959 h2hsm 27960 h2hnm 27961 hhssva 28242 hhsssm 28243 hhssnm 28244 spansnji 28633 lnopunilem1 28997 lnophmlem2 29004 stadd3i 29235 indifundif 29482 dpmul4 29750 xrsp0 29809 xrsp1 29810 hgt750lemd 30854 hgt750lem 30857 rankeq1o 32403 poimirlem8 33547 mbfposadd 33587 iocunico 38113 corcltrcl 38348 binomcxplemdvsum 38871 cosnegpi 40396 fourierdlem62 40703 fouriersw 40766 salexct3 40878 salgensscntex 40880 caragenuncllem 41047 isomenndlem 41065 |
Copyright terms: Public domain | W3C validator |