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  5411  funfvima3  5751  isoini  5819  ovg  6013  fundmen  6806  distrlem1prl  7581  distrlem1pru  7582  caucvgprprlemaddq  7707  recexgt0sr  7772  axpre-suploclemres  7900  cnegexlem2  8133  mulgt1  8820  faclbnd  10721  divgcdcoprm0  12101  cncongr2  12104  oddpwdclemdvds  12170  oddpwdclemndvds  12171  infpnlem1  12357  cnpnei  13722  zabsle1  14403