MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expdcom Structured version   Unicode version

Theorem expdcom 439
Description: Commuted form of expd 436. (Contributed by Alan Sare, 18-Mar-2012.)
Hypothesis
Ref Expression
expdcom.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expdcom  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )

Proof of Theorem expdcom
StepHypRef Expression
1 expdcom.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21expd 436 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com3l 81 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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