Theorem expcomd 1487

Description: Deduction form of expcom 116. (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 258	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  simplbi2comg  1489  2moswapdc  2171  indifdir  3477  reupick  3505  issod  4440  poxp  6428  smores2  6525  smoiun  6532  mapxpen  7101  f1dmvrnfibi  7211  recexprlemm  7939  ltleletr  8355  fzind  9693  iccid  10258  ssfzo12bi  10570  pfxccatin12lem2  11423  swrdccat  11427  dvdsabseq  12533  divalgb  12611  cncongr1  12800  difsqpwdvds  13036  lss1d  14531  txlm  15144  blsscls2  15358  metcnpi3  15382  clwwlknonex2lem2  16433