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  4039  mpteqb  5670  dffo3  5727  fconstfvm  5802  fliftfun  5865  tfrlem1  6394  tfrlem9  6405  tfr1onlemaccex  6434  tfrcllemaccex  6447  tfrcl  6450  nnsucsssuc  6578  nnaordex  6614  diffifi  6991  fidcenumlemrk  7056  fidcenumlemr  7057  nninfninc  7225  nnnninfeq  7230  nnnninfeq2  7231  exmidontriimlem4  7336  exmidontriim  7337  prarloclemup  7608  genpcdl  7632  genpcuu  7633  negf1o  8454  recexap  8726  zaddcllemneg  9411  zdiv  9461  uzaddcl  9707  fz0fzelfz0  10249  fz0fzdiffz0  10252  elfzmlbp  10254  difelfzle  10256  fzo1fzo0n0  10307  elincfzoext  10322  ssfzo12bi  10354  exfzdc  10369  zsupcllemstep  10372  modfzo0difsn  10540  frecuzrdgg  10561  seq3val  10605  seqvalcd  10606  seqf1og  10666  exp3vallem  10685  expcllem  10695  expap0  10714  mulexp  10723  swrdnd  11112  cjexp  11204  absexp  11390  fimaxre2  11538  summodc  11694  fsum2d  11746  modfsummod  11769  binom  11795  clim2prod  11850  fprod2d  11934  efexp  11993  demoivreALT  12085  divconjdvds  12160  addmodlteqALT  12170  divalglemeunn  12232  divalglemeuneg  12234  bezoutlemstep  12318  bezoutlemmain  12319  dfgcd2  12335  pw2dvdslemn  12487  oddprmdvds  12677  sgrpidmndm  13252  gsumfzz  13327  srgmulgass  13751  ringinvnzdiv  13812  lmodvsmmulgdi  14085  topbas  14539  cnplimclemr  15141  limccnp2lem  15148  gausslemma2dlem3  15540  nninfalllem1  15945  nninfsellemdc  15947  nninfsellemqall  15952  isomninnlem  15969  trirec0  15983  ismkvnnlem  15991