Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3eqtr3a | Structured version Visualization version Unicode version |
Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |
Ref | Expression |
---|---|
3eqtr3a.1 | |
3eqtr3a.2 | |
3eqtr3a.3 |
Ref | Expression |
---|---|
3eqtr3a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3a.2 | . 2 | |
2 | 3eqtr3a.1 | . . 3 | |
3 | 3eqtr3a.3 | . . 3 | |
4 | 2, 3 | syl5eq 2668 | . 2 |
5 | 1, 4 | eqtr3d 2658 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 |
This theorem is referenced by: uneqin 3878 coi2 5652 foima 6120 f1imacnv 6153 fvsnun2 6449 fnsnsplit 6450 phplem4 8142 php3 8146 rankopb 8715 fin4en1 9131 fpwwe2 9465 winacard 9514 mul02lem1 10212 cnegex2 10218 crreczi 12989 hashinf 13122 hashcard 13146 cshw0 13540 cshwn 13543 sqrtneglem 14007 rlimresb 14296 bpoly3 14789 bpoly4 14790 sinhval 14884 coshval 14885 absefib 14928 efieq1re 14929 sadcaddlem 15179 sadaddlem 15188 psgnsn 17940 odngen 17992 frlmup3 20139 mat0op 20225 restopnb 20979 cnmpt2t 21476 clmnegneg 22904 ncvspi 22956 volsup2 23373 plypf1 23968 pige3 24269 sineq0 24273 eflog 24323 logef 24328 cxpsqrt 24449 dvcncxp1 24484 cubic2 24575 quart1 24583 asinsinlem 24618 asinsin 24619 2efiatan 24645 pclogsum 24940 lgsneg 25046 numclwlk1lem2fo 27228 vc0 27429 vcm 27431 nvpi 27522 honegneg 28665 opsqrlem6 29004 sto1i 29095 mdexchi 29194 cnre2csqlem 29956 itgexpif 30684 subfacp1lem1 31161 rankaltopb 32086 poimirlem23 33432 dvtan 33460 dvasin 33496 heiborlem6 33615 trlcoat 36011 cdlemk54 36246 iocunico 37796 relintab 37889 rfovcnvf1od 38298 ntrneifv3 38380 ntrneifv4 38383 clsneifv3 38408 clsneifv4 38409 neicvgfv 38419 snunioo1 39738 dvsinexp 40125 itgsubsticclem 40191 stirlinglem1 40291 fourierdlem80 40403 fourierdlem111 40434 sqwvfoura 40445 sqwvfourb 40446 fouriersw 40448 aacllem 42547 |
Copyright terms: Public domain | W3C validator |