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  5796  dffo3  5855  fconstfvm  5933  fliftfun  6002  elabreximd  6356  tfrlem1  6579  tfrlem9  6590  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  nnsucsssuc  6765  nnaordex  6801  diffifi  7198  fidcenumlemrk  7271  fidcenumlemr  7272  nninfninc  7463  nnnninfeq  7468  nnnninfeq2  7469  exmidontriimlem4  7580  exmidontriim  7581  prarloclemup  7862  genpcdl  7886  genpcuu  7887  negf1o  8709  recexap  8981  zaddcllemneg  9683  zdiv  9734  uzaddcl  9986  fz0fzelfz0  10534  fz0fzdiffz0  10537  elfzmlbp  10539  difelfzle  10541  fzo1fzo0n0  10595  elincfzoext  10611  ssfzo12bi  10643  exfzdc  10659  zsupcllemstep  10662  modfzo0difsn  10832  frecuzrdgg  10853  seq3val  10897  seqvalcd  10898  seqf1og  10958  exp3vallem  10977  expcllem  10987  expap0  11006  mulexp  11015  swrdnd  11431  swrdswrdlem  11476  swrdswrd  11477  pfxccat3  11506  reuccatpfxs1  11519  cjexp  11658  absexp  11845  fimaxre2  11993  summodc  12150  fsum2d  12202  modfsummod  12225  binom  12251  clim2prod  12306  fprod2d  12390  efexp  12449  demoivreALT  12541  divconjdvds  12616  addmodlteqALT  12626  divalglemeunn  12688  divalglemeuneg  12690  bezoutlemstep  12774  bezoutlemmain  12775  dfgcd2  12791  pw2dvdslemn  12943  oddprmdvds  13133  sgrpidmndm  13733  srgmulgass  14293  ringinvnzdiv  14355  lmodvsmmulgdi  14660  assamulgscmlem2  15042  topbas  15168  cnplimclemr  15770  limccnp2lem  15777  gausslemma2dlem3  16182  upgriswlkdc  16601  clwwlkccatlem  16641  umgr2cwwk2dif  16665  clwwlknonex2  16680  depindlem2  16748  depindlem3  16749  nninfalllem1  17051  nninfsellemdc  17053  nninfsellemqall  17058  isomninnlem  17079  trirec0  17093  ismkvnnlem  17102