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  5727  dffo3  5784  fconstfvm  5861  fliftfun  5926  tfrlem1  6460  tfrlem9  6471  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcl  6516  nnsucsssuc  6646  nnaordex  6682  diffifi  7064  fidcenumlemrk  7132  fidcenumlemr  7133  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  exmidontriimlem4  7417  exmidontriim  7418  prarloclemup  7693  genpcdl  7717  genpcuu  7718  negf1o  8539  recexap  8811  zaddcllemneg  9496  zdiv  9546  uzaddcl  9793  fz0fzelfz0  10335  fz0fzdiffz0  10338  elfzmlbp  10340  difelfzle  10342  fzo1fzo0n0  10395  elincfzoext  10411  ssfzo12bi  10443  exfzdc  10458  zsupcllemstep  10461  modfzo0difsn  10629  frecuzrdgg  10650  seq3val  10694  seqvalcd  10695  seqf1og  10755  exp3vallem  10774  expcllem  10784  expap0  10803  mulexp  10812  swrdnd  11207  swrdswrdlem  11252  swrdswrd  11253  pfxccat3  11282  reuccatpfxs1  11295  cjexp  11420  absexp  11606  fimaxre2  11754  summodc  11910  fsum2d  11962  modfsummod  11985  binom  12011  clim2prod  12066  fprod2d  12150  efexp  12209  demoivreALT  12301  divconjdvds  12376  addmodlteqALT  12386  divalglemeunn  12448  divalglemeuneg  12450  bezoutlemstep  12534  bezoutlemmain  12535  dfgcd2  12551  pw2dvdslemn  12703  oddprmdvds  12893  sgrpidmndm  13469  gsumfzz  13544  srgmulgass  13968  ringinvnzdiv  14029  lmodvsmmulgdi  14303  topbas  14757  cnplimclemr  15359  limccnp2lem  15366  gausslemma2dlem3  15758  upgriswlkdc  16106  clwwlkccatlem  16143  umgr2cwwk2dif  16166  nninfalllem1  16462  nninfsellemdc  16464  nninfsellemqall  16469  isomninnlem  16486  trirec0  16500  ismkvnnlem  16508