![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3eqtr3ri | Structured version Visualization version GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.) |
Ref | Expression |
---|---|
3eqtr3i.1 | ⊢ 𝐴 = 𝐵 |
3eqtr3i.2 | ⊢ 𝐴 = 𝐶 |
3eqtr3i.3 | ⊢ 𝐵 = 𝐷 |
Ref | Expression |
---|---|
3eqtr3ri | ⊢ 𝐷 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3i.3 | . 2 ⊢ 𝐵 = 𝐷 | |
2 | 3eqtr3i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 3eqtr3i.2 | . . 3 ⊢ 𝐴 = 𝐶 | |
4 | 2, 3 | eqtr3i 2761 | . 2 ⊢ 𝐵 = 𝐶 |
5 | 1, 4 | eqtr3i 2761 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-cleq 2723 |
This theorem is referenced by: indif2 4270 dfif5 4544 resdm2 6230 co01 6260 funiunfv 7250 dfdom2 8980 1mhlfehlf 12438 crreczi 14198 rei 15110 bpoly3 16009 bpoly4 16010 cos1bnd 16137 rpnnen2lem3 16166 rpnnen2lem11 16174 m1bits 16388 6gcd4e2 16487 3lcm2e6 16675 karatsuba 17024 ring1 20205 sincos4thpi 26363 sincos6thpi 26365 1cubrlem 26687 cht3 27019 bclbnd 27127 bposlem8 27138 ex-ind-dvds 30148 ip1ilem 30513 mdexchi 32022 disjxpin 32253 xppreima 32305 df1stres 32359 df2ndres 32360 dpmul100 32497 0dp2dp 32509 dpmul 32513 dpmul4 32514 xrge0slmod 32900 cnrrext 33455 ballotth 34001 hgt750lemd 34125 poimirlem3 36957 poimirlem30 36984 mbfposadd 37001 asindmre 37037 refrelsredund4 37968 420gcd8e4 41340 sqmid3api 41660 areaquad 42430 inductionexd 43371 stoweidlem26 45203 3exp4mod41 46745 |
Copyright terms: Public domain | W3C validator |