Theorem expcomd 1370

Description: Deduction form of expcom 114. (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 254	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 77	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  simplbi2comg  1372  2moswapdc  2031  indifdir  3220  reupick  3248  trintssmOLD  3892  issod  4074  poxp  5873  smores2  5932  smoiun  5939  f1dmvrnfibi  6393  recexprlemm  6814  ltleletr  7193  fzind  8462  iccid  8948  ssfzo12bi  9234  dvdsabseq  10247  divalgb  10325  cncongr1  10485