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  865  3impa  1221  exp516  1254  rexlimdva2  2665  r19.29af2  2685  disjiun  4106  mpteqb  5770  dffo3  5826  fconstfvm  5904  fliftfun  5971  tfrlem1  6541  tfrlem9  6552  tfr1onlemaccex  6581  tfrcllemaccex  6594  tfrcl  6597  nnsucsssuc  6727  nnaordex  6763  diffifi  7153  fidcenumlemrk  7226  fidcenumlemr  7227  nninfninc  7416  nnnninfeq  7421  nnnninfeq2  7422  exmidontriimlem4  7533  exmidontriim  7534  prarloclemup  7812  genpcdl  7836  genpcuu  7837  negf1o  8657  recexap  8929  zaddcllemneg  9618  zdiv  9669  uzaddcl  9921  fz0fzelfz0  10465  fz0fzdiffz0  10468  elfzmlbp  10470  difelfzle  10472  fzo1fzo0n0  10526  elincfzoext  10542  ssfzo12bi  10574  exfzdc  10590  zsupcllemstep  10593  modfzo0difsn  10761  frecuzrdgg  10782  seq3val  10826  seqvalcd  10827  seqf1og  10887  exp3vallem  10906  expcllem  10916  expap0  10935  mulexp  10944  swrdnd  11355  swrdswrdlem  11400  swrdswrd  11401  pfxccat3  11430  reuccatpfxs1  11443  cjexp  11582  absexp  11768  fimaxre2  11916  summodc  12073  fsum2d  12125  modfsummod  12148  binom  12174  clim2prod  12229  fprod2d  12313  efexp  12372  demoivreALT  12464  divconjdvds  12539  addmodlteqALT  12549  divalglemeunn  12611  divalglemeuneg  12613  bezoutlemstep  12697  bezoutlemmain  12698  dfgcd2  12714  pw2dvdslemn  12866  oddprmdvds  13056  sgrpidmndm  13650  gsumfzz  13725  srgmulgass  14150  ringinvnzdiv  14211  lmodvsmmulgdi  14488  topbas  14949  cnplimclemr  15551  limccnp2lem  15558  gausslemma2dlem3  15953  upgriswlkdc  16372  clwwlkccatlem  16412  umgr2cwwk2dif  16436  clwwlknonex2  16451  depindlem2  16519  depindlem3  16520  nninfalllem1  16803  nninfsellemdc  16805  nninfsellemqall  16810  isomninnlem  16831  trirec0  16845  ismkvnnlem  16854