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

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  1493  2moswapdc  2177  indifdir  3487  reupick  3517  issod  4459  poxp  6458  smores2  6555  smoiun  6562  mapxpen  7138  f1dmvrnfibi  7248  recexprlemm  7981  ltleletr  8397  fzind  9740  iccid  10306  ssfzo12bi  10621  pfxccatin12lem2  11481  swrdccat  11485  dvdsabseq  12592  divalgb  12670  cncongr1  12859  difsqpwdvds  13095  lss1d  14692  txlm  15303  blsscls2  15517  metcnpi3  15541  clwwlknonex2lem2  16593  lealltlt1  16665