Theorem exp31 362

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 114	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
3	2	ex 114	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  exp41  368  exp42  369  expl  376  exbiri  380  anasss  397  an31s  560  con4biddc  843  3impa  1177  exp516  1209  rexlimdva2  2577  r19.29af2  2597  disjiun  3960  mpteqb  5558  dffo3  5614  fconstfvm  5685  fliftfun  5746  tfrlem1  6255  tfrlem9  6266  tfr1onlemaccex  6295  tfrcllemaccex  6308  tfrcl  6311  nnsucsssuc  6439  nnaordex  6474  diffifi  6839  fidcenumlemrk  6898  fidcenumlemr  6899  nnnninfeq  7071  nnnninfeq2  7072  exmidontriimlem4  7159  exmidontriim  7160  prarloclemup  7415  genpcdl  7439  genpcuu  7440  negf1o  8257  recexap  8527  zaddcllemneg  9206  zdiv  9252  uzaddcl  9497  fz0fzelfz0  10026  fz0fzdiffz0  10029  elfzmlbp  10031  difelfzle  10033  fzo1fzo0n0  10082  ssfzo12bi  10124  exfzdc  10139  modfzo0difsn  10294  frecuzrdgg  10315  seq3val  10357  seqvalcd  10358  exp3vallem  10420  expcllem  10430  expap0  10449  mulexp  10458  cjexp  10793  absexp  10979  fimaxre2  11126  summodc  11280  fsum2d  11332  modfsummod  11355  binom  11381  clim2prod  11436  fprod2d  11520  efexp  11579  demoivreALT  11670  divconjdvds  11741  addmodlteqALT  11751  divalglemeunn  11812  divalglemeuneg  11814  zsupcllemstep  11832  bezoutlemstep  11881  bezoutlemmain  11882  dfgcd2  11898  pw2dvdslemn  12040  topbas  12478  cnplimclemr  13049  limccnp2lem  13056  nninfalllem1  13591  nninfsellemdc  13593  nninfsellemqall  13598  isomninnlem  13612  trirec0  13626  ismkvnnlem  13634