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

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

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