Theorem exp31 364

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 115	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
3	2	ex 115	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:  exp41  370  exp42  371  expl  378  exbiri  382  anasss  399  an31s  570  con4biddc  857  3impa  1194  exp516  1227  rexlimdva2  2597  r19.29af2  2617  disjiun  3999  mpteqb  5607  dffo3  5664  fconstfvm  5735  fliftfun  5797  tfrlem1  6309  tfrlem9  6320  tfr1onlemaccex  6349  tfrcllemaccex  6362  tfrcl  6365  nnsucsssuc  6493  nnaordex  6529  diffifi  6894  fidcenumlemrk  6953  fidcenumlemr  6954  nnnninfeq  7126  nnnninfeq2  7127  exmidontriimlem4  7223  exmidontriim  7224  prarloclemup  7494  genpcdl  7518  genpcuu  7519  negf1o  8339  recexap  8610  zaddcllemneg  9292  zdiv  9341  uzaddcl  9586  fz0fzelfz0  10127  fz0fzdiffz0  10130  elfzmlbp  10132  difelfzle  10134  fzo1fzo0n0  10183  ssfzo12bi  10225  exfzdc  10240  modfzo0difsn  10395  frecuzrdgg  10416  seq3val  10458  seqvalcd  10459  exp3vallem  10521  expcllem  10531  expap0  10550  mulexp  10559  cjexp  10902  absexp  11088  fimaxre2  11235  summodc  11391  fsum2d  11443  modfsummod  11466  binom  11492  clim2prod  11547  fprod2d  11631  efexp  11690  demoivreALT  11781  divconjdvds  11855  addmodlteqALT  11865  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemstep  11946  bezoutlemstep  11998  bezoutlemmain  11999  dfgcd2  12015  pw2dvdslemn  12165  oddprmdvds  12352  sgrpidmndm  12821  srgmulgass  13172  ringinvnzdiv  13227  lmodvsmmulgdi  13413  topbas  13570  cnplimclemr  14141  limccnp2lem  14148  nninfalllem1  14760  nninfsellemdc  14762  nninfsellemqall  14767  isomninnlem  14781  trirec0  14795  ismkvnnlem  14803