Theorem expcomd 1486

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  1488  2moswapdc  2170  indifdir  3463  reupick  3491  issod  4416  poxp  6396  smores2  6459  smoiun  6466  mapxpen  7033  f1dmvrnfibi  7142  recexprlemm  7843  ltleletr  8260  fzind  9594  iccid  10159  ssfzo12bi  10469  pfxccatin12lem2  11311  swrdccat  11315  dvdsabseq  12407  divalgb  12485  cncongr1  12674  difsqpwdvds  12910  lss1d  14396  txlm  15002  blsscls2  15216  metcnpi3  15240  clwwlknonex2lem2  16288