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  862  3impa  1218  exp516  1251  rexlimdva2  2651  r19.29af2  2671  disjiun  4078  mpteqb  5725  dffo3  5782  fconstfvm  5857  fliftfun  5920  tfrlem1  6454  tfrlem9  6465  tfr1onlemaccex  6494  tfrcllemaccex  6507  tfrcl  6510  nnsucsssuc  6638  nnaordex  6674  diffifi  7056  fidcenumlemrk  7121  fidcenumlemr  7122  nninfninc  7290  nnnninfeq  7295  nnnninfeq2  7296  exmidontriimlem4  7406  exmidontriim  7407  prarloclemup  7682  genpcdl  7706  genpcuu  7707  negf1o  8528  recexap  8800  zaddcllemneg  9485  zdiv  9535  uzaddcl  9781  fz0fzelfz0  10323  fz0fzdiffz0  10326  elfzmlbp  10328  difelfzle  10330  fzo1fzo0n0  10383  elincfzoext  10399  ssfzo12bi  10431  exfzdc  10446  zsupcllemstep  10449  modfzo0difsn  10617  frecuzrdgg  10638  seq3val  10682  seqvalcd  10683  seqf1og  10743  exp3vallem  10762  expcllem  10772  expap0  10791  mulexp  10800  swrdnd  11191  swrdswrdlem  11236  swrdswrd  11237  pfxccat3  11266  reuccatpfxs1  11279  cjexp  11404  absexp  11590  fimaxre2  11738  summodc  11894  fsum2d  11946  modfsummod  11969  binom  11995  clim2prod  12050  fprod2d  12134  efexp  12193  demoivreALT  12285  divconjdvds  12360  addmodlteqALT  12370  divalglemeunn  12432  divalglemeuneg  12434  bezoutlemstep  12518  bezoutlemmain  12519  dfgcd2  12535  pw2dvdslemn  12687  oddprmdvds  12877  sgrpidmndm  13453  gsumfzz  13528  srgmulgass  13952  ringinvnzdiv  14013  lmodvsmmulgdi  14287  topbas  14741  cnplimclemr  15343  limccnp2lem  15350  gausslemma2dlem3  15742  upgriswlkdc  16071  nninfalllem1  16374  nninfsellemdc  16376  nninfsellemqall  16381  isomninnlem  16398  trirec0  16412  ismkvnnlem  16420