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  1223  xordidc  1441  f0rn0  5528  funfvima3  5883  isoini  5954  ovg  6156  fundmen  6976  distrlem1prl  7792  distrlem1pru  7793  caucvgprprlemaddq  7918  recexgt0sr  7983  axpre-suploclemres  8111  cnegexlem2  8345  mulgt1  9033  faclbnd  10993  swrdwrdsymbg  11235  pfxccatin12lem2a  11298  pfxccat3  11305  swrdccat  11306  divgcdcoprm0  12663  cncongr2  12666  oddpwdclemdvds  12732  oddpwdclemndvds  12733  infpnlem1  12922  imasabl  13913  cnpnei  14933  dvmptfsum  15439  zabsle1  15718  lgsquad2lem2  15801  2lgsoddprm  15832