Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3eqtr4ri | Structured version Visualization version GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4i.1 | ⊢ 𝐴 = 𝐵 |
3eqtr4i.2 | ⊢ 𝐶 = 𝐴 |
3eqtr4i.3 | ⊢ 𝐷 = 𝐵 |
Ref | Expression |
---|---|
3eqtr4ri | ⊢ 𝐷 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4i.3 | . . 3 ⊢ 𝐷 = 𝐵 | |
2 | 3eqtr4i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | eqtr4i 2844 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2844 | 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: cbvreucsf 3924 dfin3 4240 dfsymdif3 4266 dfif6 4466 dfsn2ALT 4577 qdass 4681 tpidm12 4683 unipr 4843 iinvdif 4993 unidif0 5251 csbcnv 5747 dfdm4 5757 dmun 5772 domepOLD 5787 resres 5859 inres 5864 resdifcom 5865 resiun1 5866 imainrect 6031 cnvcnv 6042 coundi 6093 coundir 6094 funopg 6382 csbov 7188 elrnmpores 7277 offres 7673 1st2val 7706 2nd2val 7707 mpomptsx 7751 oeoalem 8211 omopthlem1 8271 snec 8349 tcsni 9173 infmap2 9628 ackbij2lem3 9651 itunisuc 9829 axmulass 10567 divmul13i 11389 dfnn3 11640 halfpm6th 11846 numsucc 12126 decbin2 12227 uzrdgxfr 13323 hashxplem 13782 prprrab 13819 ids1 13939 s3s4 14283 s2s5 14284 s5s2 14285 fsumadd 15084 fsum2d 15114 fprodmul 15302 bpoly3 15400 bezout 15879 ressbas 16542 oppchomf 16978 oppr1 19313 opsrtoslem1 20192 m2detleiblem2 21165 txswaphmeolem 22340 cnfldnm 23314 cnrbas 23673 cnnm 23691 volres 24056 voliunlem1 24078 uniioombllem4 24114 itg11 24219 dfrelog 25076 log2ublem3 25453 bposlem8 25794 uhgrspan1 27012 ip2i 28532 bcseqi 28824 hilnormi 28867 cmcmlem 29295 fh3i 29327 fh4i 29328 pjadjii 29378 cnvoprabOLD 30382 resf1o 30392 dp3mul10 30501 dpmul4 30517 threehalves 30518 ressplusf 30564 cycpmconjs 30725 resvsca 30830 xpinpreima 31048 cnre2csqima 31053 esum2dlem 31250 eulerpartgbij 31529 ballotth 31694 plymulx 31717 hgt750lem2 31822 elrn3 32895 itg2addnclem2 34825 dfcoss3 35542 cossid 35600 dfssr2 35619 rabdif 38985 areaquad 39701 cnvrcl0 39863 stoweidlem13 42175 wallispi2 42235 fourierdlem96 42364 fourierdlem97 42365 fourierdlem98 42366 fourierdlem99 42367 fourierdlem113 42381 fourierswlem 42392 dfafv2 43208 dfnelbr2 43349 fmtnorec2 43582 fmtno5fac 43621 smndex1iidm 44001 setrec2 44726 |
Copyright terms: Public domain | W3C validator |