Theorem expdcom 455

Description: Commuted form of expd 452. (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

Step	Hyp	Ref	Expression
1		expdcom.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 452	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com3l 89	1 |- ( ps -> ( ch -> ( ph -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  odi  7659  nndi  7703  nnmass  7704  ttukeylem5  9335  genpnmax  9829  mulexp  12899  expadd  12902  expmul  12905  prmgaplem6  15760  setsstruct  15898  usgredg2vlem2  26118  usgr2trlncl  26656  clwwlksel  26914  clwwlksf1  26917  n4cyclfrgr  27155  5oalem6  28518  atom1d  29212  grpomndo  33674  pell14qrexpclnn0  37430  truniALT  38751  truniALTVD  39114  iccpartigtl  41359  sbgoldbm  41672  2zlidl  41934  rngccatidALTV  41989  ringccatidALTV  42052  nn0sumshdiglemA  42413