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

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

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