Theorem exp32 363

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 114	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	expd 256	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  exp44  371  exp45  372  expr  373  anassrs  398  an13s  557  3impb  1181  xordidc  1381  f0rn0  5363  funfvima3  5697  isoini  5765  ovg  5956  fundmen  6748  distrlem1prl  7496  distrlem1pru  7497  caucvgprprlemaddq  7622  recexgt0sr  7687  axpre-suploclemres  7815  cnegexlem2  8045  mulgt1  8728  faclbnd  10608  divgcdcoprm0  11969  cncongr2  11972  oddpwdclemdvds  12035  oddpwdclemndvds  12036  cnpnei  12590