Theorem expcomd 1421

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  1423  2moswapdc  2096  indifdir  3363  reupick  3391  issod  4278  poxp  6173  smores2  6235  smoiun  6242  mapxpen  6786  f1dmvrnfibi  6881  recexprlemm  7527  ltleletr  7942  fzind  9262  iccid  9811  ssfzo12bi  10106  dvdsabseq  11720  divalgb  11797  cncongr1  11960  txlm  12639  blsscls2  12853  metcnpi3  12877