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  859  3impa  1197  exp516  1230  rexlimdva2  2628  r19.29af2  2648  disjiun  4054  mpteqb  5693  dffo3  5750  fconstfvm  5825  fliftfun  5888  tfrlem1  6417  tfrlem9  6428  tfr1onlemaccex  6457  tfrcllemaccex  6470  tfrcl  6473  nnsucsssuc  6601  nnaordex  6637  diffifi  7017  fidcenumlemrk  7082  fidcenumlemr  7083  nninfninc  7251  nnnninfeq  7256  nnnninfeq2  7257  exmidontriimlem4  7367  exmidontriim  7368  prarloclemup  7643  genpcdl  7667  genpcuu  7668  negf1o  8489  recexap  8761  zaddcllemneg  9446  zdiv  9496  uzaddcl  9742  fz0fzelfz0  10284  fz0fzdiffz0  10287  elfzmlbp  10289  difelfzle  10291  fzo1fzo0n0  10344  elincfzoext  10359  ssfzo12bi  10391  exfzdc  10406  zsupcllemstep  10409  modfzo0difsn  10577  frecuzrdgg  10598  seq3val  10642  seqvalcd  10643  seqf1og  10703  exp3vallem  10722  expcllem  10732  expap0  10751  mulexp  10760  swrdnd  11150  swrdswrdlem  11195  swrdswrd  11196  pfxccat3  11225  reuccatpfxs1  11238  cjexp  11319  absexp  11505  fimaxre2  11653  summodc  11809  fsum2d  11861  modfsummod  11884  binom  11910  clim2prod  11965  fprod2d  12049  efexp  12108  demoivreALT  12200  divconjdvds  12275  addmodlteqALT  12285  divalglemeunn  12347  divalglemeuneg  12349  bezoutlemstep  12433  bezoutlemmain  12434  dfgcd2  12450  pw2dvdslemn  12602  oddprmdvds  12792  sgrpidmndm  13367  gsumfzz  13442  srgmulgass  13866  ringinvnzdiv  13927  lmodvsmmulgdi  14200  topbas  14654  cnplimclemr  15256  limccnp2lem  15263  gausslemma2dlem3  15655  nninfalllem1  16147  nninfsellemdc  16149  nninfsellemqall  16154  isomninnlem  16171  trirec0  16185  ismkvnnlem  16193