| 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 2768 | . 2 ⊢ 𝐷 = 𝐴 |
| 4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
| 5 | 3, 4 | eqtr4i 2768 | 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: cbvreucsf 3943 dfin3 4277 dfsymdif3 4306 rabdif 4321 dfif6 4528 dfsn2ALT 4647 qdass 4753 tpidm12 4755 iinvdif 5080 unidif0 5360 csbcnv 5894 dfdm4 5906 dmun 5921 resres 6010 inres 6015 resdifcom 6016 resiun1 6017 imainrect 6201 cnvcnv 6212 coundi 6267 coundir 6268 funopg 6600 csbov 7476 elrnmpores 7571 offres 8008 1st2val 8042 2nd2val 8043 mpomptsx 8089 oeoalem 8634 omopthlem1 8697 snec 8820 tcsni 9783 infmap2 10257 ackbij2lem3 10280 itunisuc 10459 axmulass 11197 divmul13i 12028 dfnn3 12280 halfpm6th 12487 numsucc 12773 decbin2 12874 uzrdgxfr 14008 hashxplem 14472 prprrab 14512 ids1 14635 s3s4 14972 s2s5 14973 s5s2 14974 fsumadd 15776 fsum2d 15807 fprodmul 15996 bpoly3 16094 bezout 16580 ressbasOLD 17281 oppchomf 17763 dfinito3 18050 dftermo3 18051 smndex1iidm 18914 symgbas 19389 oppr1 20350 opsrtoslem1 22079 m2detleiblem2 22634 txswaphmeolem 23812 cnfldnm 24799 cnrbas 25175 cnnm 25194 volres 25563 voliunlem1 25585 uniioombllem4 25621 itg11 25726 dfrelog 26607 log2ublem3 26991 bposlem8 27335 noinfbnd2 27776 addsasslem1 28036 uhgrspan1 29320 ip2i 30847 bcseqi 31139 hilnormi 31182 cmcmlem 31610 fh3i 31642 fh4i 31643 pjadjii 31693 resf1o 32741 dp3mul10 32880 dpmul4 32896 threehalves 32897 ressplusf 32948 cycpmconjs 33176 resvsca 33356 xpinpreima 33905 cnre2csqima 33910 esum2dlem 34093 eulerpartgbij 34374 ballotth 34540 plymulx 34563 hgt750lem2 34667 elrn3 35762 itg2addnclem2 37679 dfcoss3 38415 cossid 38481 dfssr2 38500 areaquad 43228 cnvrcl0 43638 stoweidlem13 46028 wallispi2 46088 fourierdlem96 46217 fourierdlem97 46218 fourierdlem98 46219 fourierdlem99 46220 fourierdlem113 46234 fourierswlem 46245 dfafv2 47144 dfnelbr2 47285 ceil5half3 47342 fmtnorec2 47530 fmtno5fac 47569 tposrescnv 48779 tposres3 48781 dfswapf2 48967 setrec2 49214 |
| Copyright terms: Public domain | W3C validator |