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

Theorem expdcom 437
Description: Commuted form of expd 434. (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 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com3l 81 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  odi  7220  nndi  7264  nnmass  7265  ttukeylem5  8884  genpnmax  9374  mulexp  12187  expadd  12190  expmul  12193  usgraidx2vlem2  24594  clwwlkel  24995  clwwlkf1  24998  erclwwlktr  25017  erclwwlkntr  25029  usg2wlkonot  25085  usg2spot2nb  25267  grpomndo  25546  5oalem6  26775  atom1d  27470  pell14qrexpclnn0  31041  2zlidl  32994  rngccatidALTV  33051  ringccatidALTV  33114  nn0sumshdiglemA  33494  truniALT  33702  truniALTVD  34079
  Copyright terms: Public domain W3C validator