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  847  3impa  1184  exp516  1217  rexlimdva2  2586  r19.29af2  2606  disjiun  3977  mpteqb  5576  dffo3  5632  fconstfvm  5703  fliftfun  5764  tfrlem1  6276  tfrlem9  6287  tfr1onlemaccex  6316  tfrcllemaccex  6329  tfrcl  6332  nnsucsssuc  6460  nnaordex  6495  diffifi  6860  fidcenumlemrk  6919  fidcenumlemr  6920  nnnninfeq  7092  nnnninfeq2  7093  exmidontriimlem4  7180  exmidontriim  7181  prarloclemup  7436  genpcdl  7460  genpcuu  7461  negf1o  8280  recexap  8550  zaddcllemneg  9230  zdiv  9279  uzaddcl  9524  fz0fzelfz0  10062  fz0fzdiffz0  10065  elfzmlbp  10067  difelfzle  10069  fzo1fzo0n0  10118  ssfzo12bi  10160  exfzdc  10175  modfzo0difsn  10330  frecuzrdgg  10351  seq3val  10393  seqvalcd  10394  exp3vallem  10456  expcllem  10466  expap0  10485  mulexp  10494  cjexp  10835  absexp  11021  fimaxre2  11168  summodc  11324  fsum2d  11376  modfsummod  11399  binom  11425  clim2prod  11480  fprod2d  11564  efexp  11623  demoivreALT  11714  divconjdvds  11787  addmodlteqALT  11797  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemstep  11878  bezoutlemstep  11930  bezoutlemmain  11931  dfgcd2  11947  pw2dvdslemn  12097  oddprmdvds  12284  topbas  12707  cnplimclemr  13278  limccnp2lem  13285  nninfalllem1  13888  nninfsellemdc  13890  nninfsellemqall  13895  isomninnlem  13909  trirec0  13923  ismkvnnlem  13931