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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  exp41  370  exp42  371  expl  378  exbiri  382  anasss  403  an31s  576  con4biddc  869  3impa  1225  exp516  1258  rexlimdva2  2671  r19.29af2  2691  disjiun  4125  mpteqb  5799  dffo3  5858  fconstfvm  5936  fliftfun  6005  elabreximd  6360  tfrlem1  6583  tfrlem9  6594  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcl  6639  nnsucsssuc  6769  nnaordex  6805  diffifi  7202  fidcenumlemrk  7276  fidcenumlemr  7277  nninfninc  7469  nnnninfeq  7474  nnnninfeq2  7475  exmidontriimlem4  7586  exmidontriim  7587  prarloclemup  7868  genpcdl  7892  genpcuu  7893  negf1o  8716  recexap  8989  zaddcllemneg  9694  zdiv  9745  uzaddcl  10002  fz0fzelfz0  10551  fz0fzdiffz0  10554  elfzmlbp  10556  difelfzle  10558  fzo1fzo0n0  10612  elincfzoext  10628  ssfzo12bi  10660  exfzdc  10676  zsupcllemstep  10679  modfzo0difsn  10853  frecuzrdgg  10874  seq3val  10918  seqvalcd  10919  seqf1og  10979  exp3vallem  10998  expcllem  11008  expap0  11027  mulexp  11036  swrdnd  11453  swrdswrdlem  11498  swrdswrd  11499  pfxccat3  11528  reuccatpfxs1  11541  cjexp  11680  absexp  11868  fimaxre2  12016  summodc  12175  fsum2d  12227  modfsummod  12250  binom  12276  clim2prod  12331  fprod2d  12415  efexp  12474  demoivreALT  12566  divconjdvds  12641  addmodlteqALT  12651  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemstep  12799  bezoutlemmain  12800  dfgcd2  12816  pwbdvdslemn  12969  oddprmdvds  13162  sgrpidmndm  13792  srgmulgass  14400  ringinvnzdiv  14462  lmodvsmmulgdi  14769  assamulgscmlem2  15151  topbas  15293  cnplimclemr  15895  limccnp2lem  15902  gausslemma2dlem3  16387  upgriswlkdc  16806  clwwlkccatlem  16846  umgr2cwwk2dif  16870  clwwlknonex2  16885  depindlem2  16953  depindlem3  16954  nninfalllem1  17257  nninfsellemdc  17259  nninfsellemqall  17264  isomninnlem  17285  trirec0  17300  ismkvnnlem  17309