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  567  3impb  1202  xordidc  1419  f0rn0  5492  funfvima3  5841  isoini  5910  ovg  6108  fundmen  6922  distrlem1prl  7730  distrlem1pru  7731  caucvgprprlemaddq  7856  recexgt0sr  7921  axpre-suploclemres  8049  cnegexlem2  8283  mulgt1  8971  faclbnd  10923  swrdwrdsymbg  11155  pfxccatin12lem2a  11218  pfxccat3  11225  swrdccat  11226  divgcdcoprm0  12538  cncongr2  12541  oddpwdclemdvds  12607  oddpwdclemndvds  12608  infpnlem1  12797  imasabl  13787  cnpnei  14806  dvmptfsum  15312  zabsle1  15591  lgsquad2lem2  15674  2lgsoddprm  15705