Theorem expcomd 1491

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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  simplbi2comg  1493  2moswapdc  2177  indifdir  3487  reupick  3517  issod  4464  poxp  6468  smores2  6565  smoiun  6572  mapxpen  7148  f1dmvrnfibi  7258  recexprlemm  7991  ltleletr  8407  fzind  9765  iccid  10337  ssfzo12bi  10653  pfxccatin12lem2  11517  swrdccat  11521  dvdsabseq  12630  divalgb  12708  cncongr1  12897  difsqpwdvds  13137  lss1d  14769  txlm  15429  blsscls2  15643  metcnpi3  15667  bcmono  16202  clwwlknonex2lem2  16777  lealltlt1  16849