![]() |
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 2762 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2762 | 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: cbvreucsf 3940 dfin3 4266 dfsymdif3 4296 dfif6 4531 dfsn2ALT 4648 qdass 4757 tpidm12 4759 uniprOLD 4927 iinvdif 5083 unidif0 5358 csbcnv 5883 dfdm4 5895 dmun 5910 resres 5994 inres 5999 resdifcom 6000 resiun1 6001 imainrect 6180 cnvcnv 6191 coundi 6246 coundir 6247 funopg 6582 csbov 7455 elrnmpores 7549 offres 7974 1st2val 8007 2nd2val 8008 mpomptsx 8054 oeoalem 8602 omopthlem1 8664 snec 8780 tcsni 9744 infmap2 10219 ackbij2lem3 10242 itunisuc 10420 axmulass 11158 divmul13i 11982 dfnn3 12233 halfpm6th 12440 numsucc 12724 decbin2 12825 uzrdgxfr 13939 hashxplem 14400 prprrab 14441 ids1 14554 s3s4 14891 s2s5 14892 s5s2 14893 fsumadd 15693 fsum2d 15724 fprodmul 15911 bpoly3 16009 bezout 16492 ressbasOLD 17187 oppchomf 17673 dfinito3 17965 dftermo3 17966 smndex1iidm 18824 symgbas 19286 oppr1 20248 opsrtoslem1 21927 m2detleiblem2 22450 txswaphmeolem 23628 cnfldnm 24615 cnrbas 24989 cnnm 25008 volres 25377 voliunlem1 25399 uniioombllem4 25435 itg11 25540 dfrelog 26414 log2ublem3 26794 bposlem8 27137 noinfbnd2 27577 addsasslem1 27833 uhgrspan1 28993 ip2i 30514 bcseqi 30806 hilnormi 30849 cmcmlem 31277 fh3i 31309 fh4i 31310 pjadjii 31360 cnvoprabOLD 32378 resf1o 32388 dp3mul10 32497 dpmul4 32513 threehalves 32514 ressplusf 32560 cycpmconjs 32751 resvsca 32880 xpinpreima 33350 cnre2csqima 33355 esum2dlem 33554 eulerpartgbij 33835 ballotth 34000 plymulx 34023 hgt750lem2 34128 elrn3 35202 itg2addnclem2 37004 dfcoss3 37748 cossid 37814 dfssr2 37833 rabdif 41499 areaquad 42428 cnvrcl0 42839 stoweidlem13 45188 wallispi2 45248 fourierdlem96 45377 fourierdlem97 45378 fourierdlem98 45379 fourierdlem99 45380 fourierdlem113 45394 fourierswlem 45405 dfafv2 46299 dfnelbr2 46440 fmtnorec2 46670 fmtno5fac 46709 setrec2 47902 |
Copyright terms: Public domain | W3C validator |