Theorem exp32 362

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  370  exp45  371  expr  372  anassrs  397  an13s  556  3impb  1177  xordidc  1377  f0rn0  5312  funfvima3  5644  isoini  5712  ovg  5902  fundmen  6693  distrlem1prl  7383  distrlem1pru  7384  caucvgprprlemaddq  7509  recexgt0sr  7574  axpre-suploclemres  7702  cnegexlem2  7931  mulgt1  8614  faclbnd  10480  divgcdcoprm0  11771  cncongr2  11774  oddpwdclemdvds  11837  oddpwdclemndvds  11838  cnpnei  12377