Theorem expcomd 1484

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  1486  2moswapdc  2168  indifdir  3461  reupick  3489  issod  4414  poxp  6392  smores2  6455  smoiun  6462  mapxpen  7029  f1dmvrnfibi  7134  recexprlemm  7834  ltleletr  8251  fzind  9585  iccid  10150  ssfzo12bi  10460  pfxccatin12lem2  11302  swrdccat  11306  dvdsabseq  12398  divalgb  12476  cncongr1  12665  difsqpwdvds  12901  lss1d  14387  txlm  14993  blsscls2  15207  metcnpi3  15231  clwwlknonex2lem2  16233