Theorem exp32 363

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 114	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	expd 256	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  exp44  371  exp45  372  expr  373  anassrs  398  an13s  557  3impb  1189  xordidc  1389  f0rn0  5382  funfvima3  5718  isoini  5786  ovg  5980  fundmen  6772  distrlem1prl  7523  distrlem1pru  7524  caucvgprprlemaddq  7649  recexgt0sr  7714  axpre-suploclemres  7842  cnegexlem2  8074  mulgt1  8758  faclbnd  10654  divgcdcoprm0  12033  cncongr2  12036  oddpwdclemdvds  12102  oddpwdclemndvds  12103  infpnlem1  12289  cnpnei  12859  zabsle1  13540