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  7992  ltleletr  8408  fzind  9766  iccid  10338  ssfzo12bi  10654  pfxccatin12lem2  11519  swrdccat  11523  dvdsabseq  12633  divalgb  12711  cncongr1  12900  difsqpwdvds  13140  lss1d  14804  txlm  15471  blsscls2  15685  metcnpi3  15709  bcmono  16265  clwwlknonex2lem2  16845  lealltlt1  16917