Theorem expcomd 1429

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simplbi2comg  1431  2moswapdc  2104  indifdir  3378  reupick  3406  issod  4297  poxp  6200  smores2  6262  smoiun  6269  mapxpen  6814  f1dmvrnfibi  6909  recexprlemm  7565  ltleletr  7980  fzind  9306  iccid  9861  ssfzo12bi  10160  dvdsabseq  11785  divalgb  11862  cncongr1  12035  difsqpwdvds  12269  txlm  12919  blsscls2  13133  metcnpi3  13157