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  569  3impb  1225  xordidc  1443  f0rn0  5531  funfvima3  5887  isoini  5958  ovg  6160  fundmen  6980  distrlem1prl  7801  distrlem1pru  7802  caucvgprprlemaddq  7927  recexgt0sr  7992  axpre-suploclemres  8120  cnegexlem2  8354  mulgt1  9042  faclbnd  11002  swrdwrdsymbg  11244  pfxccatin12lem2a  11307  pfxccat3  11314  swrdccat  11315  divgcdcoprm0  12672  cncongr2  12675  oddpwdclemdvds  12741  oddpwdclemndvds  12742  infpnlem1  12931  imasabl  13922  cnpnei  14942  dvmptfsum  15448  zabsle1  15727  lgsquad2lem2  15810  2lgsoddprm  15841