Theorem expcomd 1452

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  1454  2moswapdc  2132  indifdir  3416  reupick  3444  issod  4351  poxp  6287  smores2  6349  smoiun  6356  mapxpen  6906  f1dmvrnfibi  7005  recexprlemm  7686  ltleletr  8103  fzind  9435  iccid  9994  ssfzo12bi  10295  dvdsabseq  11992  divalgb  12069  cncongr1  12244  difsqpwdvds  12479  lss1d  13882  txlm  14458  blsscls2  14672  metcnpi3  14696