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  2135  indifdir  3419  reupick  3447  issod  4354  poxp  6290  smores2  6352  smoiun  6359  mapxpen  6909  f1dmvrnfibi  7010  recexprlemm  7691  ltleletr  8108  fzind  9441  iccid  10000  ssfzo12bi  10301  dvdsabseq  12012  divalgb  12090  cncongr1  12271  difsqpwdvds  12507  lss1d  13939  txlm  14515  blsscls2  14729  metcnpi3  14753