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  843  3impa  1177  exp516  1206  rexlimdva2  2555  r19.29af2  2575  disjiun  3932  mpteqb  5519  dffo3  5575  fconstfvm  5646  fliftfun  5705  tfrlem1  6213  tfrlem9  6224  tfr1onlemaccex  6253  tfrcllemaccex  6266  tfrcl  6269  nnsucsssuc  6396  nnaordex  6431  diffifi  6796  fidcenumlemrk  6850  fidcenumlemr  6851  prarloclemup  7327  genpcdl  7351  genpcuu  7352  negf1o  8168  recexap  8438  zaddcllemneg  9117  zdiv  9163  uzaddcl  9408  fz0fzelfz0  9935  fz0fzdiffz0  9938  elfzmlbp  9940  difelfzle  9942  fzo1fzo0n0  9991  ssfzo12bi  10033  exfzdc  10048  modfzo0difsn  10199  frecuzrdgg  10220  seq3val  10262  seqvalcd  10263  exp3vallem  10325  expcllem  10335  expap0  10354  mulexp  10363  cjexp  10697  absexp  10883  fimaxre2  11030  summodc  11184  fsum2d  11236  modfsummod  11259  binom  11285  clim2prod  11340  efexp  11425  demoivreALT  11516  divconjdvds  11583  addmodlteqALT  11593  divalglemeunn  11654  divalglemeuneg  11656  zsupcllemstep  11674  bezoutlemstep  11721  bezoutlemmain  11722  dfgcd2  11738  pw2dvdslemn  11879  topbas  12275  cnplimclemr  12846  limccnp2lem  12853  nninfalllemn  13377  nninfalllem1  13378  nninfsellemdc  13381  nninfsellemqall  13386  isomninnlem  13400  trirec0  13412  ismkvnnlem  13419