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  5520  funfvima3  5873  isoini  5942  ovg  6144  fundmen  6959  distrlem1prl  7769  distrlem1pru  7770  caucvgprprlemaddq  7895  recexgt0sr  7960  axpre-suploclemres  8088  cnegexlem2  8322  mulgt1  9010  faclbnd  10963  swrdwrdsymbg  11196  pfxccatin12lem2a  11259  pfxccat3  11266  swrdccat  11267  divgcdcoprm0  12623  cncongr2  12626  oddpwdclemdvds  12692  oddpwdclemndvds  12693  infpnlem1  12882  imasabl  13873  cnpnei  14893  dvmptfsum  15399  zabsle1  15678  lgsquad2lem2  15761  2lgsoddprm  15792