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  572  con4biddc  864  3impa  1220  exp516  1253  rexlimdva2  2653  r19.29af2  2673  disjiun  4083  mpteqb  5737  dffo3  5794  fconstfvm  5871  fliftfun  5936  tfrlem1  6473  tfrlem9  6484  tfr1onlemaccex  6513  tfrcllemaccex  6526  tfrcl  6529  nnsucsssuc  6659  nnaordex  6695  diffifi  7082  fidcenumlemrk  7152  fidcenumlemr  7153  nninfninc  7321  nnnninfeq  7326  nnnninfeq2  7327  exmidontriimlem4  7438  exmidontriim  7439  prarloclemup  7714  genpcdl  7738  genpcuu  7739  negf1o  8560  recexap  8832  zaddcllemneg  9517  zdiv  9567  uzaddcl  9819  fz0fzelfz0  10361  fz0fzdiffz0  10364  elfzmlbp  10366  difelfzle  10368  fzo1fzo0n0  10421  elincfzoext  10437  ssfzo12bi  10469  exfzdc  10485  zsupcllemstep  10488  modfzo0difsn  10656  frecuzrdgg  10677  seq3val  10721  seqvalcd  10722  seqf1og  10782  exp3vallem  10801  expcllem  10811  expap0  10830  mulexp  10839  swrdnd  11239  swrdswrdlem  11284  swrdswrd  11285  pfxccat3  11314  reuccatpfxs1  11327  cjexp  11453  absexp  11639  fimaxre2  11787  summodc  11943  fsum2d  11995  modfsummod  12018  binom  12044  clim2prod  12099  fprod2d  12183  efexp  12242  demoivreALT  12334  divconjdvds  12409  addmodlteqALT  12419  divalglemeunn  12481  divalglemeuneg  12483  bezoutlemstep  12567  bezoutlemmain  12568  dfgcd2  12584  pw2dvdslemn  12736  oddprmdvds  12926  sgrpidmndm  13502  gsumfzz  13577  srgmulgass  14001  ringinvnzdiv  14062  lmodvsmmulgdi  14336  topbas  14790  cnplimclemr  15392  limccnp2lem  15399  gausslemma2dlem3  15791  upgriswlkdc  16210  clwwlkccatlem  16250  umgr2cwwk2dif  16274  clwwlknonex2  16289  nninfalllem1  16610  nninfsellemdc  16612  nninfsellemqall  16617  isomninnlem  16634  trirec0  16648  ismkvnnlem  16656