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  5872  fliftfun  5937  tfrlem1  6474  tfrlem9  6485  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcl  6530  nnsucsssuc  6660  nnaordex  6696  diffifi  7083  fidcenumlemrk  7153  fidcenumlemr  7154  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  exmidontriimlem4  7439  exmidontriim  7440  prarloclemup  7715  genpcdl  7739  genpcuu  7740  negf1o  8561  recexap  8833  zaddcllemneg  9518  zdiv  9568  uzaddcl  9820  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  fzo1fzo0n0  10422  elincfzoext  10438  ssfzo12bi  10470  exfzdc  10486  zsupcllemstep  10489  modfzo0difsn  10657  frecuzrdgg  10678  seq3val  10722  seqvalcd  10723  seqf1og  10783  exp3vallem  10802  expcllem  10812  expap0  10831  mulexp  10840  swrdnd  11240  swrdswrdlem  11285  swrdswrd  11286  pfxccat3  11315  reuccatpfxs1  11328  cjexp  11454  absexp  11640  fimaxre2  11788  summodc  11945  fsum2d  11997  modfsummod  12020  binom  12046  clim2prod  12101  fprod2d  12185  efexp  12244  demoivreALT  12336  divconjdvds  12411  addmodlteqALT  12421  divalglemeunn  12483  divalglemeuneg  12485  bezoutlemstep  12569  bezoutlemmain  12570  dfgcd2  12586  pw2dvdslemn  12738  oddprmdvds  12928  sgrpidmndm  13504  gsumfzz  13579  srgmulgass  14004  ringinvnzdiv  14065  lmodvsmmulgdi  14339  topbas  14793  cnplimclemr  15395  limccnp2lem  15402  gausslemma2dlem3  15794  upgriswlkdc  16213  clwwlkccatlem  16253  umgr2cwwk2dif  16277  clwwlknonex2  16292  nninfalllem1  16613  nninfsellemdc  16615  nninfsellemqall  16620  isomninnlem  16637  trirec0  16651  ismkvnnlem  16659