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  1202  xordidc  1419  f0rn0  5470  funfvima3  5818  isoini  5887  ovg  6085  fundmen  6898  distrlem1prl  7695  distrlem1pru  7696  caucvgprprlemaddq  7821  recexgt0sr  7886  axpre-suploclemres  8014  cnegexlem2  8248  mulgt1  8936  faclbnd  10886  swrdwrdsymbg  11117  divgcdcoprm0  12423  cncongr2  12426  oddpwdclemdvds  12492  oddpwdclemndvds  12493  infpnlem1  12682  imasabl  13672  cnpnei  14691  dvmptfsum  15197  zabsle1  15476  lgsquad2lem2  15559  2lgsoddprm  15590