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  5317  funfvima3  5651  isoini  5719  ovg  5909  fundmen  6700  distrlem1prl  7390  distrlem1pru  7391  caucvgprprlemaddq  7516  recexgt0sr  7581  axpre-suploclemres  7709  cnegexlem2  7938  mulgt1  8621  faclbnd  10487  divgcdcoprm0  11782  cncongr2  11785  oddpwdclemdvds  11848  oddpwdclemndvds  11849  cnpnei  12388