![]() |
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 2824 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2824 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-cleq 2791 |
This theorem is referenced by: cbvreucsf 3872 dfin3 4193 dfsymdif3 4221 dfif6 4428 dfsn2ALT 4545 qdass 4649 tpidm12 4651 unipr 4817 iinvdif 4965 unidif0 5225 csbcnv 5718 dfdm4 5728 dmun 5743 domepOLD 5758 resres 5831 inres 5836 resdifcom 5837 resiun1 5838 imainrect 6005 cnvcnv 6016 coundi 6067 coundir 6068 funopg 6358 csbov 7178 elrnmpores 7267 offres 7666 1st2val 7699 2nd2val 7700 mpomptsx 7744 oeoalem 8205 omopthlem1 8265 snec 8343 tcsni 9169 infmap2 9629 ackbij2lem3 9652 itunisuc 9830 axmulass 10568 divmul13i 11390 dfnn3 11639 halfpm6th 11846 numsucc 12126 decbin2 12227 uzrdgxfr 13330 hashxplem 13790 prprrab 13827 ids1 13942 s3s4 14286 s2s5 14287 s5s2 14288 fsumadd 15088 fsum2d 15118 fprodmul 15306 bpoly3 15404 bezout 15881 ressbas 16546 oppchomf 16982 smndex1iidm 18058 symgbas 18491 oppr1 19380 opsrtoslem1 20723 m2detleiblem2 21233 txswaphmeolem 22409 cnfldnm 23384 cnrbas 23747 cnnm 23765 volres 24132 voliunlem1 24154 uniioombllem4 24190 itg11 24295 dfrelog 25157 log2ublem3 25534 bposlem8 25875 uhgrspan1 27093 ip2i 28611 bcseqi 28903 hilnormi 28946 cmcmlem 29374 fh3i 29406 fh4i 29407 pjadjii 29457 cnvoprabOLD 30482 resf1o 30492 dp3mul10 30600 dpmul4 30616 threehalves 30617 ressplusf 30663 cycpmconjs 30848 resvsca 30954 xpinpreima 31259 cnre2csqima 31264 esum2dlem 31461 eulerpartgbij 31740 ballotth 31905 plymulx 31928 hgt750lem2 32033 elrn3 33111 itg2addnclem2 35109 dfcoss3 35822 cossid 35880 dfssr2 35899 rabdif 39399 areaquad 40166 cnvrcl0 40325 stoweidlem13 42655 wallispi2 42715 fourierdlem96 42844 fourierdlem97 42845 fourierdlem98 42846 fourierdlem99 42847 fourierdlem113 42861 fourierswlem 42872 dfafv2 43688 dfnelbr2 43829 fmtnorec2 44060 fmtno5fac 44099 setrec2 45225 |
Copyright terms: Public domain | W3C validator |