| 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 2767 | . 2 ⊢ 𝐵 = 𝐶 |
| 5 | 1, 4 | eqtr3i 2767 | 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 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 |
| This theorem is referenced by: indif2 4281 dfif5 4542 resdm2 6251 co01 6281 funiunfv 7268 dfdom2 9018 1mhlfehlf 12485 crreczi 14267 rei 15195 bpoly3 16094 bpoly4 16095 cos1bnd 16223 rpnnen2lem3 16252 rpnnen2lem11 16260 m1bits 16477 6gcd4e2 16575 3lcm2e6 16769 karatsuba 17121 ring1 20307 sincos4thpi 26555 sincos6thpi 26558 1cubrlem 26884 cht3 27216 bclbnd 27324 bposlem8 27335 ex-ind-dvds 30480 ip1ilem 30845 mdexchi 32354 disjxpin 32601 xppreima 32655 df1stres 32713 df2ndres 32714 dpmul100 32879 0dp2dp 32891 dpmul 32895 dpmul4 32896 xrge0slmod 33376 cnrrext 34011 ballotth 34540 hgt750lemd 34663 poimirlem3 37630 poimirlem30 37657 mbfposadd 37674 asindmre 37710 refrelsredund4 38633 420gcd8e4 42007 sqmid3api 42318 areaquad 43228 inductionexd 44168 stoweidlem26 46041 3exp4mod41 47603 tposresg 48778 |
| Copyright terms: Public domain | W3C validator |