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  7365  nnnninfeq  7370  nnnninfeq2  7371  exmidontriimlem4  7482  exmidontriim  7483  prarloclemup  7758  genpcdl  7782  genpcuu  7783  negf1o  8603  recexap  8875  zaddcllemneg  9562  zdiv  9612  uzaddcl  9864  fz0fzelfz0  10407  fz0fzdiffz0  10410  elfzmlbp  10412  difelfzle  10414  fzo1fzo0n0  10468  elincfzoext  10484  ssfzo12bi  10516  exfzdc  10532  zsupcllemstep  10535  modfzo0difsn  10703  frecuzrdgg  10724  seq3val  10768  seqvalcd  10769  seqf1og  10829  exp3vallem  10848  expcllem  10858  expap0  10877  mulexp  10886  swrdnd  11289  swrdswrdlem  11334  swrdswrd  11335  pfxccat3  11364  reuccatpfxs1  11377  cjexp  11516  absexp  11702  fimaxre2  11850  summodc  12007  fsum2d  12059  modfsummod  12082  binom  12108  clim2prod  12163  fprod2d  12247  efexp  12306  demoivreALT  12398  divconjdvds  12473  addmodlteqALT  12483  divalglemeunn  12545  divalglemeuneg  12547  bezoutlemstep  12631  bezoutlemmain  12632  dfgcd2  12648  pw2dvdslemn  12800  oddprmdvds  12990  sgrpidmndm  13566  gsumfzz  13641  srgmulgass  14066  ringinvnzdiv  14127  lmodvsmmulgdi  14402  topbas  14861  cnplimclemr  15463  limccnp2lem  15470  gausslemma2dlem3  15865  upgriswlkdc  16284  clwwlkccatlem  16324  umgr2cwwk2dif  16348  clwwlknonex2  16363  depindlem2  16431  depindlem3  16432  nninfalllem1  16717  nninfsellemdc  16719  nninfsellemqall  16724  isomninnlem  16745  trirec0  16759  ismkvnnlem  16768