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  562  3impb  1194  xordidc  1394  f0rn0  5392  funfvima3  5729  isoini  5797  ovg  5991  fundmen  6784  distrlem1prl  7544  distrlem1pru  7545  caucvgprprlemaddq  7670  recexgt0sr  7735  axpre-suploclemres  7863  cnegexlem2  8095  mulgt1  8779  faclbnd  10675  divgcdcoprm0  12055  cncongr2  12058  oddpwdclemdvds  12124  oddpwdclemndvds  12125  infpnlem1  12311  cnpnei  13013  zabsle1  13694