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  1199  xordidc  1399  f0rn0  5407  funfvima3  5746  isoini  5814  ovg  6008  fundmen  6801  distrlem1prl  7576  distrlem1pru  7577  caucvgprprlemaddq  7702  recexgt0sr  7767  axpre-suploclemres  7895  cnegexlem2  8127  mulgt1  8814  faclbnd  10712  divgcdcoprm0  12091  cncongr2  12094  oddpwdclemdvds  12160  oddpwdclemndvds  12161  infpnlem1  12347  cnpnei  13501  zabsle1  14182