![]() |
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 2852 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2852 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 df-cleq 2818 |
This theorem is referenced by: cbvreucsf 3791 dfin3 4096 dfsymdif3 4122 dfif6 4309 dfsn2ALT 4417 qdass 4506 tpidm12 4508 unipr 4671 iinvdif 4812 unidif0 5060 csbcnv 5538 dfdm4 5548 dmun 5563 resres 5646 inres 5651 resdifcom 5652 resiun1 5653 imainrect 5816 cnvcnv 5827 coundi 5877 coundir 5878 funopg 6157 csbov 6947 elrnmpt2res 7034 offres 7423 1st2val 7456 2nd2val 7457 mpt2mptsx 7496 oeoalem 7943 omopthlem1 8002 snec 8075 tcsni 8896 infmap2 9355 ackbij2lem3 9378 itunisuc 9556 axmulass 10294 divmul13i 11112 dfnn3 11366 halfpm6th 11579 numsucc 11862 decbin2 11964 uzrdgxfr 13061 hashxplem 13509 prprrab 13544 ids1 13657 s3s4 14054 s2s5 14055 s5s2 14056 fsumadd 14847 fsum2d 14877 fprodmul 15063 bpoly3 15161 bezout 15633 ressbas 16293 oppchomf 16732 oppr1 18988 opsrtoslem1 19844 m2detleiblem2 20802 cnfldnm 22952 cnnm 23329 volres 23694 voliunlem1 23716 uniioombllem4 23752 itg11 23857 plyid 24364 coeidp 24418 dgrid 24419 dfrelog 24711 log2ublem3 25088 bposlem8 25429 uhgrspan1 26600 ip2i 28238 bcseqi 28532 hilnormi 28575 cmcmlem 29005 fh3i 29037 fh4i 29038 pjadjii 29088 cnvoprabOLD 30046 resf1o 30053 dp3mul10 30151 dpmul4 30167 threehalves 30168 ressplusf 30195 resvsca 30375 xpinpreima 30497 cnre2csqima 30502 esum2dlem 30699 eulerpartgbij 30979 ballotth 31145 plymulx 31172 hgt750lem2 31279 elrn3 32194 domep 32236 itg2addnclem2 34005 dfcoss3 34720 cossid 34778 dfssr2 34797 areaquad 38644 cnvrcl0 38773 stoweidlem13 41024 wallispi2 41084 fourierdlem96 41213 fourierdlem97 41214 fourierdlem98 41215 fourierdlem99 41216 fourierdlem113 41230 fourierswlem 41241 dfafv2 42034 dfnelbr2 42175 fmtnorec2 42285 fmtno5fac 42324 setrec2 43337 |
Copyright terms: Public domain | W3C validator |