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  5587  funfvima3  5952  isoini  6024  ovg  6228  fundmen  7094  distrlem1prl  7950  distrlem1pru  7951  caucvgprprlemaddq  8076  recexgt0sr  8141  axpre-suploclemres  8269  cnegexlem2  8504  mulgt1  9196  faclbnd  11195  swrdwrdsymbg  11452  pfxccatin12lem2a  11515  pfxccat3  11522  swrdccat  11523  divgcdcoprm0  12898  cncongr2  12901  nnmaxpwlemdvds  12968  nnmaxpwlemndvds  12969  infpnlem1  13161  imasabl  14224  cnpnei  15411  dvmptfsum  15917  zabsle1  16284  lgsquad2lem2  16367  2lgsoddprm  16398  eupth2lemsfi  16885