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  8710  recexap  8983  zaddcllemneg  9687  zdiv  9738  uzaddcl  9995  fz0fzelfz0  10544  fz0fzdiffz0  10547  elfzmlbp  10549  difelfzle  10551  fzo1fzo0n0  10605  elincfzoext  10621  ssfzo12bi  10653  exfzdc  10669  zsupcllemstep  10672  modfzo0difsn  10845  frecuzrdgg  10866  seq3val  10910  seqvalcd  10911  seqf1og  10971  exp3vallem  10990  expcllem  11000  expap0  11019  mulexp  11028  swrdnd  11445  swrdswrdlem  11490  swrdswrd  11491  pfxccat3  11520  reuccatpfxs1  11533  cjexp  11672  absexp  11860  fimaxre2  12008  summodc  12166  fsum2d  12218  modfsummod  12241  binom  12267  clim2prod  12322  fprod2d  12406  efexp  12465  demoivreALT  12557  divconjdvds  12632  addmodlteqALT  12642  divalglemeunn  12704  divalglemeuneg  12706  bezoutlemstep  12790  bezoutlemmain  12791  dfgcd2  12807  pwbdvdslemn  12960  oddprmdvds  13153  sgrpidmndm  13782  srgmulgass  14342  ringinvnzdiv  14404  lmodvsmmulgdi  14709  assamulgscmlem2  15091  topbas  15217  cnplimclemr  15819  limccnp2lem  15826  gausslemma2dlem3  16280  upgriswlkdc  16699  clwwlkccatlem  16739  umgr2cwwk2dif  16763  clwwlknonex2  16778  depindlem2  16846  depindlem3  16847  nninfalllem1  17149  nninfsellemdc  17151  nninfsellemqall  17156  isomninnlem  17177  trirec0  17191  ismkvnnlem  17200