Theorem exp31 362

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp31.1	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
exp31	|- ( ph -> ( ps -> ( ch -> th ) ) )

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	ex 114	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
3	2	ex 114	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:  exp41  368  exp42  369  expl  376  exbiri  380  anasss  397  an31s  565  con4biddc  852  3impa  1189  exp516  1222  rexlimdva2  2590  r19.29af2  2610  disjiun  3984  mpteqb  5586  dffo3  5643  fconstfvm  5714  fliftfun  5775  tfrlem1  6287  tfrlem9  6298  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfrcl  6343  nnsucsssuc  6471  nnaordex  6507  diffifi  6872  fidcenumlemrk  6931  fidcenumlemr  6932  nnnninfeq  7104  nnnninfeq2  7105  exmidontriimlem4  7201  exmidontriim  7202  prarloclemup  7457  genpcdl  7481  genpcuu  7482  negf1o  8301  recexap  8571  zaddcllemneg  9251  zdiv  9300  uzaddcl  9545  fz0fzelfz0  10083  fz0fzdiffz0  10086  elfzmlbp  10088  difelfzle  10090  fzo1fzo0n0  10139  ssfzo12bi  10181  exfzdc  10196  modfzo0difsn  10351  frecuzrdgg  10372  seq3val  10414  seqvalcd  10415  exp3vallem  10477  expcllem  10487  expap0  10506  mulexp  10515  cjexp  10857  absexp  11043  fimaxre2  11190  summodc  11346  fsum2d  11398  modfsummod  11421  binom  11447  clim2prod  11502  fprod2d  11586  efexp  11645  demoivreALT  11736  divconjdvds  11809  addmodlteqALT  11819  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemstep  11900  bezoutlemstep  11952  bezoutlemmain  11953  dfgcd2  11969  pw2dvdslemn  12119  oddprmdvds  12306  sgrpidmndm  12656  topbas  12861  cnplimclemr  13432  limccnp2lem  13439  nninfalllem1  14041  nninfsellemdc  14043  nninfsellemqall  14048  isomninnlem  14062  trirec0  14076  ismkvnnlem  14084