Theorem exp32 365

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp32.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
exp32	|- ( ph -> ( ps -> ( ch -> th ) ) )

Proof of Theorem exp32

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	ex 115	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	expd 258	1 |- ( ph -> ( ps -> ( ch -> 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:  exp44  373  exp45  374  expr  375  anassrs  404  an13s  573  3impb  1230  xordidc  1448  f0rn0  5590  funfvima3  5955  isoini  6027  ovg  6231  fundmen  7100  distrlem1prl  7955  distrlem1pru  7956  caucvgprprlemaddq  8081  recexgt0sr  8146  axpre-suploclemres  8274  cnegexlem2  8509  mulgt1  9201  faclbnd  11200  swrdwrdsymbg  11457  pfxccatin12lem2a  11520  pfxccat3  11527  swrdccat  11528  divgcdcoprm0  12903  cncongr2  12906  nnmaxpwlemdvds  12973  nnmaxpwlemndvds  12974  infpnlem1  13166  imasabl  14229  cnpnei  15462  dvmptfsum  15968  zabsle1  16340  lgsquad2lem2  16423  2lgsoddprm  16454  eupth2lemsfi  16941