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  572  con4biddc  865  3impa  1221  exp516  1254  rexlimdva2  2654  r19.29af2  2674  disjiun  4088  mpteqb  5746  dffo3  5802  fconstfvm  5880  fliftfun  5947  tfrlem1  6517  tfrlem9  6528  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcl  6573  nnsucsssuc  6703  nnaordex  6739  diffifi  7126  fidcenumlemrk  7196  fidcenumlemr  7197  nninfninc  7382  nnnninfeq  7387  nnnninfeq2  7388  exmidontriimlem4  7499  exmidontriim  7500  prarloclemup  7775  genpcdl  7799  genpcuu  7800  negf1o  8620  recexap  8892  zaddcllemneg  9579  zdiv  9629  uzaddcl  9881  fz0fzelfz0  10424  fz0fzdiffz0  10427  elfzmlbp  10429  difelfzle  10431  fzo1fzo0n0  10485  elincfzoext  10501  ssfzo12bi  10533  exfzdc  10549  zsupcllemstep  10552  modfzo0difsn  10720  frecuzrdgg  10741  seq3val  10785  seqvalcd  10786  seqf1og  10846  exp3vallem  10865  expcllem  10875  expap0  10894  mulexp  10903  swrdnd  11306  swrdswrdlem  11351  swrdswrd  11352  pfxccat3  11381  reuccatpfxs1  11394  cjexp  11533  absexp  11719  fimaxre2  11867  summodc  12024  fsum2d  12076  modfsummod  12099  binom  12125  clim2prod  12180  fprod2d  12264  efexp  12323  demoivreALT  12415  divconjdvds  12490  addmodlteqALT  12500  divalglemeunn  12562  divalglemeuneg  12564  bezoutlemstep  12648  bezoutlemmain  12649  dfgcd2  12665  pw2dvdslemn  12817  oddprmdvds  13007  sgrpidmndm  13583  gsumfzz  13658  srgmulgass  14083  ringinvnzdiv  14144  lmodvsmmulgdi  14419  topbas  14878  cnplimclemr  15480  limccnp2lem  15487  gausslemma2dlem3  15882  upgriswlkdc  16301  clwwlkccatlem  16341  umgr2cwwk2dif  16365  clwwlknonex2  16380  depindlem2  16448  depindlem3  16449  nninfalllem1  16734  nninfsellemdc  16736  nninfsellemqall  16741  isomninnlem  16762  trirec0  16776  ismkvnnlem  16785