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  1223  xordidc  1441  f0rn0  5522  funfvima3  5877  isoini  5948  ovg  6150  fundmen  6967  distrlem1prl  7780  distrlem1pru  7781  caucvgprprlemaddq  7906  recexgt0sr  7971  axpre-suploclemres  8099  cnegexlem2  8333  mulgt1  9021  faclbnd  10975  swrdwrdsymbg  11212  pfxccatin12lem2a  11275  pfxccat3  11282  swrdccat  11283  divgcdcoprm0  12639  cncongr2  12642  oddpwdclemdvds  12708  oddpwdclemndvds  12709  infpnlem1  12898  imasabl  13889  cnpnei  14909  dvmptfsum  15415  zabsle1  15694  lgsquad2lem2  15777  2lgsoddprm  15808