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  404  an13s  573  3impb  1230  xordidc  1448  f0rn0  5582  funfvima3  5942  isoini  6014  ovg  6218  fundmen  7084  distrlem1prl  7939  distrlem1pru  7940  caucvgprprlemaddq  8065  recexgt0sr  8130  axpre-suploclemres  8258  cnegexlem2  8492  mulgt1  9183  faclbnd  11157  swrdwrdsymbg  11414  pfxccatin12lem2a  11477  pfxccat3  11484  swrdccat  11485  divgcdcoprm0  12857  cncongr2  12860  oddpwdclemdvds  12926  oddpwdclemndvds  12927  infpnlem1  13116  imasabl  14117  cnpnei  15243  dvmptfsum  15749  zabsle1  16032  lgsquad2lem2  16115  2lgsoddprm  16146  eupth2lemsfi  16633