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  858  3impa  1196  exp516  1229  rexlimdva2  2617  r19.29af2  2637  disjiun  4028  mpteqb  5652  dffo3  5709  fconstfvm  5780  fliftfun  5843  tfrlem1  6366  tfrlem9  6377  tfr1onlemaccex  6406  tfrcllemaccex  6419  tfrcl  6422  nnsucsssuc  6550  nnaordex  6586  diffifi  6955  fidcenumlemrk  7020  fidcenumlemr  7021  nninfninc  7189  nnnninfeq  7194  nnnninfeq2  7195  exmidontriimlem4  7291  exmidontriim  7292  prarloclemup  7562  genpcdl  7586  genpcuu  7587  negf1o  8408  recexap  8680  zaddcllemneg  9365  zdiv  9414  uzaddcl  9660  fz0fzelfz0  10202  fz0fzdiffz0  10205  elfzmlbp  10207  difelfzle  10209  fzo1fzo0n0  10259  ssfzo12bi  10301  exfzdc  10316  zsupcllemstep  10319  modfzo0difsn  10487  frecuzrdgg  10508  seq3val  10552  seqvalcd  10553  seqf1og  10613  exp3vallem  10632  expcllem  10642  expap0  10661  mulexp  10670  cjexp  11058  absexp  11244  fimaxre2  11392  summodc  11548  fsum2d  11600  modfsummod  11623  binom  11649  clim2prod  11704  fprod2d  11788  efexp  11847  demoivreALT  11939  divconjdvds  12014  addmodlteqALT  12024  divalglemeunn  12086  divalglemeuneg  12088  bezoutlemstep  12164  bezoutlemmain  12165  dfgcd2  12181  pw2dvdslemn  12333  oddprmdvds  12523  sgrpidmndm  13061  gsumfzz  13127  srgmulgass  13545  ringinvnzdiv  13606  lmodvsmmulgdi  13879  topbas  14303  cnplimclemr  14905  limccnp2lem  14912  gausslemma2dlem3  15304  nninfalllem1  15652  nninfsellemdc  15654  nninfsellemqall  15659  isomninnlem  15674  trirec0  15688  ismkvnnlem  15696