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  859  3impa  1197  exp516  1230  rexlimdva2  2626  r19.29af2  2646  disjiun  4040  mpteqb  5672  dffo3  5729  fconstfvm  5804  fliftfun  5867  tfrlem1  6396  tfrlem9  6407  tfr1onlemaccex  6436  tfrcllemaccex  6449  tfrcl  6452  nnsucsssuc  6580  nnaordex  6616  diffifi  6993  fidcenumlemrk  7058  fidcenumlemr  7059  nninfninc  7227  nnnninfeq  7232  nnnninfeq2  7233  exmidontriimlem4  7338  exmidontriim  7339  prarloclemup  7610  genpcdl  7634  genpcuu  7635  negf1o  8456  recexap  8728  zaddcllemneg  9413  zdiv  9463  uzaddcl  9709  fz0fzelfz0  10251  fz0fzdiffz0  10254  elfzmlbp  10256  difelfzle  10258  fzo1fzo0n0  10309  elincfzoext  10324  ssfzo12bi  10356  exfzdc  10371  zsupcllemstep  10374  modfzo0difsn  10542  frecuzrdgg  10563  seq3val  10607  seqvalcd  10608  seqf1og  10668  exp3vallem  10687  expcllem  10697  expap0  10716  mulexp  10725  swrdnd  11115  cjexp  11237  absexp  11423  fimaxre2  11571  summodc  11727  fsum2d  11779  modfsummod  11802  binom  11828  clim2prod  11883  fprod2d  11967  efexp  12026  demoivreALT  12118  divconjdvds  12193  addmodlteqALT  12203  divalglemeunn  12265  divalglemeuneg  12267  bezoutlemstep  12351  bezoutlemmain  12352  dfgcd2  12368  pw2dvdslemn  12520  oddprmdvds  12710  sgrpidmndm  13285  gsumfzz  13360  srgmulgass  13784  ringinvnzdiv  13845  lmodvsmmulgdi  14118  topbas  14572  cnplimclemr  15174  limccnp2lem  15181  gausslemma2dlem3  15573  nninfalllem1  15982  nninfsellemdc  15984  nninfsellemqall  15989  isomninnlem  16006  trirec0  16020  ismkvnnlem  16028