Theorem expcomd 1452

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  1454  2moswapdc  2132  indifdir  3415  reupick  3443  issod  4350  poxp  6285  smores2  6347  smoiun  6354  mapxpen  6904  f1dmvrnfibi  7003  recexprlemm  7684  ltleletr  8101  fzind  9432  iccid  9991  ssfzo12bi  10292  dvdsabseq  11989  divalgb  12066  cncongr1  12241  difsqpwdvds  12476  lss1d  13879  txlm  14447  blsscls2  14661  metcnpi3  14685