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  3460  reupick  3488  issod  4409  poxp  6376  smores2  6438  smoiun  6445  mapxpen  7005  f1dmvrnfibi  7107  recexprlemm  7807  ltleletr  8224  fzind  9558  iccid  10117  ssfzo12bi  10426  pfxccatin12lem2  11258  swrdccat  11262  dvdsabseq  12353  divalgb  12431  cncongr1  12620  difsqpwdvds  12856  lss1d  14341  txlm  14947  blsscls2  15161  metcnpi3  15185