Theorem expcomd 1417

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  1419  2moswapdc  2087  indifdir  3327  reupick  3355  issod  4236  poxp  6122  smores2  6184  smoiun  6191  mapxpen  6735  f1dmvrnfibi  6825  recexprlemm  7425  ltleletr  7839  fzind  9159  iccid  9701  ssfzo12bi  9995  dvdsabseq  11534  divalgb  11611  cncongr1  11773  txlm  12437  blsscls2  12651  metcnpi3  12675