Theorem expcomd 1491

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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  simplbi2comg  1493  2moswapdc  2177  indifdir  3487  reupick  3517  issod  4464  poxp  6468  smores2  6565  smoiun  6572  mapxpen  7148  f1dmvrnfibi  7258  recexprlemm  7991  ltleletr  8407  fzind  9761  iccid  10327  ssfzo12bi  10643  pfxccatin12lem2  11503  swrdccat  11507  dvdsabseq  12614  divalgb  12692  cncongr1  12881  difsqpwdvds  13117  lss1d  14720  txlm  15380  blsscls2  15594  metcnpi3  15618  clwwlknonex2lem2  16679  lealltlt1  16751