Theorem expcomd 1434

Description: Deduction form of expcom 115. (Contributed by Alan Sare, 22-Jul-2012.)

Hypothesis

Ref	Expression
expcomd.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
expcomd	|- ( ph -> ( ch -> ( ps -> th ) ) )

Proof of Theorem expcomd

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 256	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  simplbi2comg  1436  2moswapdc  2109  indifdir  3383  reupick  3411  issod  4304  poxp  6211  smores2  6273  smoiun  6280  mapxpen  6826  f1dmvrnfibi  6921  recexprlemm  7586  ltleletr  8001  fzind  9327  iccid  9882  ssfzo12bi  10181  dvdsabseq  11807  divalgb  11884  cncongr1  12057  difsqpwdvds  12291  txlm  13073  blsscls2  13287  metcnpi3  13311