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 2843 | . 2 ⊢ 𝐵 = 𝐶 |
5 | 1, 4 | eqtr3i 2843 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 |
This theorem is referenced by: indif2 4244 dfif5 4479 resdm2 6081 co01 6107 funiunfv 6998 dfdom2 8523 1mhlfehlf 11844 crreczi 13577 rei 14503 bpoly3 15400 bpoly4 15401 cos1bnd 15528 rpnnen2lem3 15557 rpnnen2lem11 15565 m1bits 15777 6gcd4e2 15874 3lcm2e6 16060 karatsuba 16408 ring1 19281 sincos4thpi 25026 sincos6thpi 25028 1cubrlem 25346 cht3 25677 bclbnd 25783 bposlem8 25794 ex-ind-dvds 28167 ip1ilem 28530 mdexchi 30039 disjxpin 30266 xppreima 30322 df1stres 30365 df2ndres 30366 dpmul100 30500 0dp2dp 30512 dpmul 30516 dpmul4 30517 xrge0slmod 30844 cnrrext 31150 ballotth 31694 hgt750lemd 31818 poimirlem3 34776 poimirlem30 34803 mbfposadd 34820 asindmre 34858 refrelsredund4 35747 sqmid3api 39047 areaquad 39701 inductionexd 40383 stoweidlem26 42188 3exp4mod41 43658 |
Copyright terms: Public domain | W3C validator |