Theorem expcomd 1462

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  1464  2moswapdc  2145  indifdir  3433  reupick  3461  issod  4374  poxp  6331  smores2  6393  smoiun  6400  mapxpen  6960  f1dmvrnfibi  7061  recexprlemm  7757  ltleletr  8174  fzind  9508  iccid  10067  ssfzo12bi  10376  dvdsabseq  12233  divalgb  12311  cncongr1  12500  difsqpwdvds  12736  lss1d  14220  txlm  14826  blsscls2  15040  metcnpi3  15064