Theorem expcomd 1371

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  1373  2moswapdc  2032  indifdir  3227  reupick  3255  trintssmOLD  3900  issod  4082  poxp  5884  smores2  5943  smoiun  5950  f1dmvrnfibi  6452  recexprlemm  6876  ltleletr  7260  fzind  8543  iccid  9024  ssfzo12bi  9311  dvdsabseq  10392  divalgb  10469  cncongr1  10629