Theorem expcomd 1484

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  1486  2moswapdc  2168  indifdir  3460  reupick  3488  issod  4410  poxp  6384  smores2  6446  smoiun  6453  mapxpen  7017  f1dmvrnfibi  7122  recexprlemm  7822  ltleletr  8239  fzind  9573  iccid  10133  ssfzo12bi  10443  pfxccatin12lem2  11278  swrdccat  11282  dvdsabseq  12373  divalgb  12451  cncongr1  12640  difsqpwdvds  12876  lss1d  14362  txlm  14968  blsscls2  15182  metcnpi3  15206