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  6584  tfrlem9  6595  tfr1onlemaccex  6624  tfrcllemaccex  6637  tfrcl  6640  nnsucsssuc  6770  nnaordex  6806  diffifi  7204  fidcenumlemrk  7278  fidcenumlemr  7279  nninfninc  7469  nnnninfeq  7474  nnnninfeq2  7475  exmidontriimlem4  7586  exmidontriim  7587  prarloclemup  7868  genpcdl  7892  genpcuu  7893  negf1o  8716  recexap  8989  zaddcllemneg  9692  zdiv  9744  uzaddcl  10001  fz0fzelfz0  10550  fz0fzdiffz0  10553  elfzmlbp  10555  difelfzle  10557  fzo1fzo0n0  10611  elincfzoext  10627  ssfzo12bi  10659  exfzdc  10675  zsupcllemstep  10678  modfzo0difsn  10852  frecuzrdgg  10873  seq3val  10917  seqvalcd  10918  seqf1og  10978  exp3vallem  10997  expcllem  11007  expap0  11026  mulexp  11035  swrdnd  11452  swrdswrdlem  11497  swrdswrd  11498  pfxccat3  11527  reuccatpfxs1  11540  cjexp  11679  absexp  11867  fimaxre2  12015  summodc  12174  fsum2d  12226  modfsummod  12249  binom  12275  clim2prod  12330  fprod2d  12414  efexp  12473  demoivreALT  12565  divconjdvds  12640  addmodlteqALT  12650  divalglemeunn  12712  divalglemeuneg  12714  bezoutlemstep  12798  bezoutlemmain  12799  dfgcd2  12815  pwbdvdslemn  12968  oddprmdvds  13161  sgrpidmndm  13791  srgmulgass  14399  ringinvnzdiv  14461  lmodvsmmulgdi  14768  assamulgscmlem2  15150  topbas  15310  cnplimclemr  15912  limccnp2lem  15919  gausslemma2dlem3  16404  upgriswlkdc  16823  clwwlkccatlem  16863  umgr2cwwk2dif  16887  clwwlknonex2  16902  depindlem2  16970  depindlem3  16971  nninfalllem1  17274  nninfsellemdc  17276  nninfsellemqall  17281  isomninnlem  17302  trirec0  17317  ismkvnnlem  17326