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  4466  poxp  6472  smores2  6570  smoiun  6577  mapxpen  7154  f1dmvrnfibi  7264  recexprlemm  7997  ltleletr  8413  fzind  9771  iccid  10343  ssfzo12bi  10659  pfxccatin12lem2  11524  swrdccat  11528  dvdsabseq  12638  divalgb  12716  cncongr1  12905  difsqpwdvds  13145  lss1d  14828  txlm  15522  blsscls2  15736  metcnpi3  15760  bcmono  16321  clwwlknonex2lem2  16901  lealltlt1  16973