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 ) ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  exp44  373  exp45  374  expr  375  anassrs  400  an13s  569  3impb  1226  xordidc  1444  f0rn0  5562  funfvima3  5920  isoini  5991  ovg  6193  fundmen  7047  distrlem1prl  7897  distrlem1pru  7898  caucvgprprlemaddq  8023  recexgt0sr  8088  axpre-suploclemres  8216  cnegexlem2  8449  mulgt1  9137  faclbnd  11103  swrdwrdsymbg  11356  pfxccatin12lem2a  11419  pfxccat3  11426  swrdccat  11427  divgcdcoprm0  12798  cncongr2  12801  oddpwdclemdvds  12867  oddpwdclemndvds  12868  infpnlem1  13057  imasabl  14053  cnpnei  15084  dvmptfsum  15590  zabsle1  15872  lgsquad2lem2  15955  2lgsoddprm  15986  eupth2lemsfi  16473