![]() |
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 2508 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtr3d 2498 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-cleq 2455 |
This theorem is referenced by: uneqin 3706 coi2 5375 foima 5825 f1imacnv 5857 fvsnun2 6129 fnsnsplit 6130 phplem4 7785 php3 7789 rankopb 8354 fin4en1 8770 fpwwe2 9099 winacard 9148 mul02lem1 9840 cnegex2 9846 crreczi 12435 hashinf 12558 hashcard 12575 cshw0 12939 cshwn 12942 sqrtneglem 13385 rlimresb 13684 bpoly3 14166 bpoly4 14167 sinhval 14263 coshval 14264 absefib 14307 efieq1re 14308 sadcaddlem 14486 sadaddlem 14495 psgnsn 17216 odngen 17281 frlmup3 19413 mat0op 19499 restopnb 20246 cnmpt2t 20743 volsup2 22619 plypf1 23222 pige3 23528 sineq0 23532 eflog 23582 logef 23587 cxpsqrt 23704 dvcncxp1 23739 cubic2 23830 quart1 23838 asinsinlem 23873 asinsin 23874 2efiatan 23900 pclogsum 24199 lgsneg 24303 numclwlk1lem2fo 25879 vc0 26244 vcm 26246 vcnegneg 26249 nvpi 26351 honegneg 27515 opsqrlem6 27854 sto1i 27945 mdexchi 28044 cnre2csqlem 28767 subfacp1lem1 29952 ghomfo 30359 rankaltopb 30796 poimirlem23 32009 dvtan 32038 dvasin 32074 heiborlem6 32194 trlcoat 34336 cdlemk54 34571 iocunico 36141 relintab 36235 snunioo1 37698 dvsinexp 37866 itgsubsticclem 37938 stirlinglem1 38037 fourierdlem80 38151 fourierdlem111 38182 sqwvfoura 38193 sqwvfourb 38194 fouriersw 38196 aacllem 40909 |
Copyright terms: Public domain | W3C validator |