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  862  3impa  1218  exp516  1251  rexlimdva2  2651  r19.29af2  2671  disjiun  4081  mpteqb  5733  dffo3  5790  fconstfvm  5867  fliftfun  5932  tfrlem1  6469  tfrlem9  6480  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcl  6525  nnsucsssuc  6655  nnaordex  6691  diffifi  7076  fidcenumlemrk  7144  fidcenumlemr  7145  nninfninc  7313  nnnninfeq  7318  nnnninfeq2  7319  exmidontriimlem4  7429  exmidontriim  7430  prarloclemup  7705  genpcdl  7729  genpcuu  7730  negf1o  8551  recexap  8823  zaddcllemneg  9508  zdiv  9558  uzaddcl  9810  fz0fzelfz0  10352  fz0fzdiffz0  10355  elfzmlbp  10357  difelfzle  10359  fzo1fzo0n0  10412  elincfzoext  10428  ssfzo12bi  10460  exfzdc  10476  zsupcllemstep  10479  modfzo0difsn  10647  frecuzrdgg  10668  seq3val  10712  seqvalcd  10713  seqf1og  10773  exp3vallem  10792  expcllem  10802  expap0  10821  mulexp  10830  swrdnd  11230  swrdswrdlem  11275  swrdswrd  11276  pfxccat3  11305  reuccatpfxs1  11318  cjexp  11444  absexp  11630  fimaxre2  11778  summodc  11934  fsum2d  11986  modfsummod  12009  binom  12035  clim2prod  12090  fprod2d  12174  efexp  12233  demoivreALT  12325  divconjdvds  12400  addmodlteqALT  12410  divalglemeunn  12472  divalglemeuneg  12474  bezoutlemstep  12558  bezoutlemmain  12559  dfgcd2  12575  pw2dvdslemn  12727  oddprmdvds  12917  sgrpidmndm  13493  gsumfzz  13568  srgmulgass  13992  ringinvnzdiv  14053  lmodvsmmulgdi  14327  topbas  14781  cnplimclemr  15383  limccnp2lem  15390  gausslemma2dlem3  15782  upgriswlkdc  16157  clwwlkccatlem  16195  umgr2cwwk2dif  16219  clwwlknonex2  16234  nninfalllem1  16546  nninfsellemdc  16548  nninfsellemqall  16553  isomninnlem  16570  trirec0  16584  ismkvnnlem  16592