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  3998  mpteqb  5606  dffo3  5663  fconstfvm  5734  fliftfun  5796  tfrlem1  6308  tfrlem9  6319  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfrcl  6364  nnsucsssuc  6492  nnaordex  6528  diffifi  6893  fidcenumlemrk  6952  fidcenumlemr  6953  nnnninfeq  7125  nnnninfeq2  7126  exmidontriimlem4  7222  exmidontriim  7223  prarloclemup  7493  genpcdl  7517  genpcuu  7518  negf1o  8337  recexap  8608  zaddcllemneg  9290  zdiv  9339  uzaddcl  9584  fz0fzelfz0  10124  fz0fzdiffz0  10127  elfzmlbp  10129  difelfzle  10131  fzo1fzo0n0  10180  ssfzo12bi  10222  exfzdc  10237  modfzo0difsn  10392  frecuzrdgg  10413  seq3val  10455  seqvalcd  10456  exp3vallem  10518  expcllem  10528  expap0  10547  mulexp  10556  cjexp  10897  absexp  11083  fimaxre2  11230  summodc  11386  fsum2d  11438  modfsummod  11461  binom  11487  clim2prod  11542  fprod2d  11626  efexp  11685  demoivreALT  11776  divconjdvds  11849  addmodlteqALT  11859  divalglemeunn  11920  divalglemeuneg  11922  zsupcllemstep  11940  bezoutlemstep  11992  bezoutlemmain  11993  dfgcd2  12009  pw2dvdslemn  12159  oddprmdvds  12346  sgrpidmndm  12775  srgmulgass  13125  ringinvnzdiv  13180  topbas  13460  cnplimclemr  14031  limccnp2lem  14038  nninfalllem1  14639  nninfsellemdc  14641  nninfsellemqall  14646  isomninnlem  14660  trirec0  14674  ismkvnnlem  14682