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  5455  funfvima3  5799  isoini  5868  ovg  6066  fundmen  6874  distrlem1prl  7666  distrlem1pru  7667  caucvgprprlemaddq  7792  recexgt0sr  7857  axpre-suploclemres  7985  cnegexlem2  8219  mulgt1  8907  faclbnd  10850  divgcdcoprm0  12294  cncongr2  12297  oddpwdclemdvds  12363  oddpwdclemndvds  12364  infpnlem1  12553  imasabl  13542  cnpnei  14539  dvmptfsum  15045  zabsle1  15324  lgsquad2lem2  15407  2lgsoddprm  15438