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  1201  xordidc  1410  f0rn0  5452  funfvima3  5796  isoini  5865  ovg  6062  fundmen  6865  distrlem1prl  7649  distrlem1pru  7650  caucvgprprlemaddq  7775  recexgt0sr  7840  axpre-suploclemres  7968  cnegexlem2  8202  mulgt1  8890  faclbnd  10833  divgcdcoprm0  12269  cncongr2  12272  oddpwdclemdvds  12338  oddpwdclemndvds  12339  infpnlem1  12528  imasabl  13466  cnpnei  14455  dvmptfsum  14961  zabsle1  15240  lgsquad2lem2  15323  2lgsoddprm  15354