![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 3eqtr3a | 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 2510 | . 2 |
5 | 1, 4 | eqtr3d 2500 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 = wceq 1395 |
This theorem is referenced by: uneqin 3748 coi2 5529 foima 5805 f1imacnv 5837 fvsnun2 6107 fnsnsplit 6108 phplem4 7719 php3 7723 rankopb 8291 fin4en1 8710 fpwwe2 9042 winacard 9091 mul02lem1 9777 cnegex2 9783 crreczi 12291 hashinf 12410 hashcard 12427 cshw0 12765 cshwn 12768 sqrtneglem 13100 rlimresb 13388 sinhval 13889 coshval 13890 absefib 13933 efieq1re 13934 sadcaddlem 14107 sadaddlem 14116 psgnsn 16545 odngen 16597 frlmup3 18834 mat0op 18921 restopnb 19676 cnmpt2t 20174 volsup2 22014 plypf1 22609 pige3 22910 sineq0 22914 eflog 22964 logef 22966 cxpsqrt 23084 cubic2 23179 quart1 23187 asinsinlem 23222 asinsin 23223 2efiatan 23249 pclogsum 23490 lgsneg 23594 numclwlk1lem2fo 25095 vc0 25462 vcm 25464 vcnegneg 25467 nvpi 25569 honegneg 26725 opsqrlem6 27064 sto1i 27155 mdexchi 27254 cnre2csqlem 27892 subfacp1lem1 28623 ghomfo 29031 rankaltopb 29629 bpoly3 29820 bpoly4 29821 dvtan 30065 dvcncxp1 30100 dvasin 30103 heiborlem6 30312 iocunico 31178 snunioo1 31552 dvsinexp 31705 itgsubsticclem 31774 stirlinglem1 31856 fourierdlem80 31969 fourierdlem111 32000 sqwvfoura 32011 sqwvfourb 32012 fouriersw 32014 aacllem 33216 trlcoat 36449 cdlemk54 36684 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-cleq 2449 |
Copyright terms: Public domain | W3C validator |