Theorem expcomd 1487

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  1489  2moswapdc  2170  indifdir  3465  reupick  3493  issod  4422  poxp  6406  smores2  6503  smoiun  6510  mapxpen  7077  f1dmvrnfibi  7186  recexprlemm  7887  ltleletr  8303  fzind  9639  iccid  10204  ssfzo12bi  10516  pfxccatin12lem2  11361  swrdccat  11365  dvdsabseq  12471  divalgb  12549  cncongr1  12738  difsqpwdvds  12974  lss1d  14462  txlm  15073  blsscls2  15287  metcnpi3  15311  clwwlknonex2lem2  16362