Theorem expcomd 1418

Description: Deduction form of expcom 115. (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 256	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  simplbi2comg  1420  2moswapdc  2090  indifdir  3337  reupick  3365  issod  4249  poxp  6137  smores2  6199  smoiun  6206  mapxpen  6750  f1dmvrnfibi  6840  recexprlemm  7456  ltleletr  7870  fzind  9190  iccid  9738  ssfzo12bi  10033  dvdsabseq  11581  divalgb  11658  cncongr1  11820  txlm  12487  blsscls2  12701  metcnpi3  12725