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  6569  smoiun  6576  mapxpen  7152  f1dmvrnfibi  7262  recexprlemm  7997  ltleletr  8413  fzind  9772  iccid  10344  ssfzo12bi  10660  pfxccatin12lem2  11525  swrdccat  11529  dvdsabseq  12639  divalgb  12717  cncongr1  12906  difsqpwdvds  13146  lss1d  14829  txlm  15505  blsscls2  15719  metcnpi3  15743  bcmono  16304  clwwlknonex2lem2  16884  lealltlt1  16956