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  5888  isoini  5959  ovg  6161  fundmen  6981  distrlem1prl  7802  distrlem1pru  7803  caucvgprprlemaddq  7928  recexgt0sr  7993  axpre-suploclemres  8121  cnegexlem2  8355  mulgt1  9043  faclbnd  11004  swrdwrdsymbg  11249  pfxccatin12lem2a  11312  pfxccat3  11319  swrdccat  11320  divgcdcoprm0  12691  cncongr2  12694  oddpwdclemdvds  12760  oddpwdclemndvds  12761  infpnlem1  12950  imasabl  13941  cnpnei  14962  dvmptfsum  15468  zabsle1  15747  lgsquad2lem2  15830  2lgsoddprm  15861  eupth2lemsfi  16348