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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  exp41  370  exp42  371  expl  378  exbiri  382  anasss  403  an31s  576  con4biddc  869  3impa  1225  exp516  1258  rexlimdva2  2671  r19.29af2  2691  disjiun  4125  mpteqb  5796  dffo3  5855  fconstfvm  5933  fliftfun  6002  elabreximd  6356  tfrlem1  6579  tfrlem9  6590  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  nnsucsssuc  6765  nnaordex  6801  diffifi  7198  fidcenumlemrk  7271  fidcenumlemr  7272  nninfninc  7464  nnnninfeq  7469  nnnninfeq2  7470  exmidontriimlem4  7581  exmidontriim  7582  prarloclemup  7863  genpcdl  7887  genpcuu  7888  negf1o  8711  recexap  8984  zaddcllemneg  9688  zdiv  9739  uzaddcl  9996  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzmlbp  10550  difelfzle  10552  fzo1fzo0n0  10606  elincfzoext  10622  ssfzo12bi  10654  exfzdc  10670  zsupcllemstep  10673  modfzo0difsn  10847  frecuzrdgg  10868  seq3val  10912  seqvalcd  10913  seqf1og  10973  exp3vallem  10992  expcllem  11002  expap0  11021  mulexp  11030  swrdnd  11447  swrdswrdlem  11492  swrdswrd  11493  pfxccat3  11522  reuccatpfxs1  11535  cjexp  11674  absexp  11862  fimaxre2  12010  summodc  12169  fsum2d  12221  modfsummod  12244  binom  12270  clim2prod  12325  fprod2d  12409  efexp  12468  demoivreALT  12560  divconjdvds  12635  addmodlteqALT  12645  divalglemeunn  12707  divalglemeuneg  12709  bezoutlemstep  12793  bezoutlemmain  12794  dfgcd2  12810  pwbdvdslemn  12963  oddprmdvds  13156  sgrpidmndm  13786  srgmulgass  14377  ringinvnzdiv  14439  lmodvsmmulgdi  14744  assamulgscmlem2  15126  topbas  15259  cnplimclemr  15861  limccnp2lem  15868  gausslemma2dlem3  16348  upgriswlkdc  16767  clwwlkccatlem  16807  umgr2cwwk2dif  16831  clwwlknonex2  16846  depindlem2  16914  depindlem3  16915  nninfalllem1  17217  nninfsellemdc  17219  nninfsellemqall  17224  isomninnlem  17245  trirec0  17260  ismkvnnlem  17269