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  1226  xordidc  1444  f0rn0  5540  funfvima3  5898  isoini  5969  ovg  6171  fundmen  7024  distrlem1prl  7862  distrlem1pru  7863  caucvgprprlemaddq  7988  recexgt0sr  8053  axpre-suploclemres  8181  cnegexlem2  8414  mulgt1  9102  faclbnd  11066  swrdwrdsymbg  11311  pfxccatin12lem2a  11374  pfxccat3  11381  swrdccat  11382  divgcdcoprm0  12753  cncongr2  12756  oddpwdclemdvds  12822  oddpwdclemndvds  12823  infpnlem1  13012  imasabl  14003  cnpnei  15030  dvmptfsum  15536  zabsle1  15818  lgsquad2lem2  15901  2lgsoddprm  15932  eupth2lemsfi  16419