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 2632 | . 2 ⊢ 𝐴 = 𝐶 |
4 | 3eqtri.3 | . 2 ⊢ 𝐶 = 𝐷 | |
5 | 3, 4 | eqtr2i 2633 | 1 ⊢ 𝐷 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 |
This theorem is referenced by: dfif5 4052 resindm 5364 difxp1 5478 difxp2 5479 dfdm2 5584 cofunex2g 7024 df1st2 7150 df2nd2 7151 domss2 8004 adderpqlem 9655 dfn2 11182 9p1e10 11372 sq10OLD 12913 sqrtm1 13864 0.999... 14451 0.999...OLD 14452 pockthi 15449 matgsum 20062 indistps 20625 indistps2 20626 refun0 21128 filcon 21497 sincosq3sgn 24056 sincosq4sgn 24057 eff1o 24099 ax5seglem7 25615 clwlknclwlkdifs 26487 cnnvg 26917 cnnvs 26919 cnnvnm 26920 h2hva 27215 h2hsm 27216 h2hnm 27217 hhssva 27498 hhsssm 27499 hhssnm 27500 spansnji 27889 lnopunilem1 28253 lnophmlem2 28260 stadd3i 28491 indifundif 28740 xrsp0 29012 xrsp1 29013 rankeq1o 31448 poimirlem8 32587 mbfposadd 32627 iocunico 36815 corcltrcl 37050 binomcxplemdvsum 37576 cosnegpi 38750 fourierdlem62 39061 fouriersw 39124 salexct3 39236 salgensscntex 39238 caragenuncllem 39402 isomenndlem 39420 0grsubgr 40502 nbupgrres 40592 clwwlknclwwlkdifs 41181 |
Copyright terms: Public domain | W3C validator |