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

Theorem expdcom 445
Description: Commuted form of expd 442. (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 442 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com3l 84 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  odi  7267  nndi  7311  nnmass  7312  ttukeylem5  8930  genpnmax  9419  mulexp  12305  expadd  12308  expmul  12311  prmgaplem6  15037  usgraidx2vlem2  25131  clwwlkel  25533  clwwlkf1  25536  erclwwlktr  25555  erclwwlkntr  25567  usg2wlkonot  25623  usg2spot2nb  25805  grpomndo  26086  5oalem6  27324  atom1d  28018  pell14qrexpclnn0  35714  truniALT  36903  truniALTVD  37272  iccpartigtl  38828  usgredg2vlem2  39405  2zlidl  40259  rngccatidALTV  40316  ringccatidALTV  40379  nn0sumshdiglemA  40755
  Copyright terms: Public domain W3C validator