![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > expdcom | Structured version Unicode version |
Description: Commuted form of expd 436. (Contributed by Alan Sare, 18-Mar-2012.) |
Ref | Expression |
---|---|
expdcom.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
expdcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expdcom.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | expd 436 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | com3l 81 |
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 |
This theorem depends on definitions: df-bi 185 df-an 371 |
This theorem is referenced by: odi 7123 nndi 7167 nnmass 7168 ttukeylem5 8788 genpnmax 9282 mulexp 12015 expadd 12018 expmul 12021 usgraidx2vlem2 23457 grpomndo 23980 5oalem6 25209 atom1d 25904 pell14qrexpclnn0 29350 usg2wlkonot 30545 clwwlkel 30598 clwwlkf1 30601 erclwwlktr 30628 erclwwlkntr 30644 usg2spot2nb 30801 truniALT 31561 truniALTVD 31927 |
Copyright terms: Public domain | W3C validator |