Theorem exp31 361

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  367  exp42  368  expl  375  exbiri  379  anasss  396  an31s  559  con4biddc  842  3impa  1176  exp516  1205  rexlimdva2  2550  r19.29af2  2570  disjiun  3919  mpteqb  5504  dffo3  5560  fconstfvm  5631  fliftfun  5690  tfrlem1  6198  tfrlem9  6209  tfr1onlemaccex  6238  tfrcllemaccex  6251  tfrcl  6254  nnsucsssuc  6381  nnaordex  6416  diffifi  6781  fidcenumlemrk  6835  fidcenumlemr  6836  prarloclemup  7296  genpcdl  7320  genpcuu  7321  negf1o  8137  recexap  8407  zaddcllemneg  9086  zdiv  9132  uzaddcl  9374  fz0fzelfz0  9897  fz0fzdiffz0  9900  elfzmlbp  9902  difelfzle  9904  fzo1fzo0n0  9953  ssfzo12bi  9995  exfzdc  10010  modfzo0difsn  10161  frecuzrdgg  10182  seq3val  10224  seqvalcd  10225  exp3vallem  10287  expcllem  10297  expap0  10316  mulexp  10325  cjexp  10658  absexp  10844  fimaxre2  10991  summodc  11145  fsum2d  11197  modfsummod  11220  binom  11246  clim2prod  11301  efexp  11377  demoivreALT  11469  divconjdvds  11536  addmodlteqALT  11546  divalglemeunn  11607  divalglemeuneg  11609  zsupcllemstep  11627  bezoutlemstep  11674  bezoutlemmain  11675  dfgcd2  11691  pw2dvdslemn  11832  topbas  12225  cnplimclemr  12796  limccnp2lem  12803  nninfalllemn  13191  nninfalllem1  13192  nninfsellemdc  13195  nninfsellemqall  13200  isomninnlem  13214