![]() |
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 2804 | . 2 ⊢ 𝐵 = 𝐶 |
5 | 1, 4 | eqtr3i 2804 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-cleq 2770 |
This theorem is referenced by: indif2 4097 dfif5 4323 resdm2 5880 co01 5906 funiunfv 6780 dfdom2 8269 1mhlfehlf 11606 crreczi 13313 rei 14309 bpoly3 15200 bpoly4 15201 cos1bnd 15328 rpnnen2lem3 15358 rpnnen2lem11 15366 m1bits 15578 6gcd4e2 15671 3lcm2e6 15855 karatsuba 16203 ring1 19000 sincos4thpi 24714 sincos6thpi 24716 1cubrlem 25030 cht3 25362 bclbnd 25468 bposlem8 25479 ex-ind-dvds 27910 ip1ilem 28270 mdexchi 29783 disjxpin 29981 xppreima 30031 df1stres 30064 df2ndres 30065 dpmul100 30181 0dp2dp 30193 dpmul 30197 dpmul4 30198 xrge0slmod 30414 cnrrext 30660 ballotth 31206 hgt750lemd 31336 poimirlem3 34047 poimirlem30 34074 mbfposadd 34091 asindmre 34129 refrelsred4 35010 sqmid3api 38159 areaquad 38774 inductionexd 39423 stoweidlem26 41184 3exp4mod41 42568 |
Copyright terms: Public domain | W3C validator |