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  1201  xordidc  1410  f0rn0  5449  funfvima3  5793  isoini  5862  ovg  6059  fundmen  6862  distrlem1prl  7644  distrlem1pru  7645  caucvgprprlemaddq  7770  recexgt0sr  7835  axpre-suploclemres  7963  cnegexlem2  8197  mulgt1  8884  faclbnd  10815  divgcdcoprm0  12242  cncongr2  12245  oddpwdclemdvds  12311  oddpwdclemndvds  12312  infpnlem1  12500  imasabl  13409  cnpnei  14398  dvmptfsum  14904  zabsle1  15156  lgsquad2lem2  15239  2lgsoddprm  15270