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  403  an31s  576  con4biddc  869  3impa  1225  exp516  1258  rexlimdva2  2671  r19.29af2  2691  disjiun  4123  mpteqb  5793  dffo3  5849  fconstfvm  5927  fliftfun  5995  elabreximd  6349  tfrlem1  6572  tfrlem9  6583  tfr1onlemaccex  6612  tfrcllemaccex  6625  tfrcl  6628  nnsucsssuc  6758  nnaordex  6794  diffifi  7191  fidcenumlemrk  7264  fidcenumlemr  7265  nninfninc  7456  nnnninfeq  7461  nnnninfeq2  7462  exmidontriimlem4  7573  exmidontriim  7574  prarloclemup  7855  genpcdl  7879  genpcuu  7880  negf1o  8702  recexap  8974  zaddcllemneg  9665  zdiv  9716  uzaddcl  9968  fz0fzelfz0  10515  fz0fzdiffz0  10518  elfzmlbp  10520  difelfzle  10522  fzo1fzo0n0  10576  elincfzoext  10592  ssfzo12bi  10624  exfzdc  10640  zsupcllemstep  10643  modfzo0difsn  10813  frecuzrdgg  10834  seq3val  10878  seqvalcd  10879  seqf1og  10939  exp3vallem  10958  expcllem  10968  expap0  10987  mulexp  10996  swrdnd  11412  swrdswrdlem  11457  swrdswrd  11458  pfxccat3  11487  reuccatpfxs1  11500  cjexp  11639  absexp  11826  fimaxre2  11974  summodc  12131  fsum2d  12183  modfsummod  12206  binom  12232  clim2prod  12287  fprod2d  12371  efexp  12430  demoivreALT  12522  divconjdvds  12597  addmodlteqALT  12607  divalglemeunn  12669  divalglemeuneg  12671  bezoutlemstep  12755  bezoutlemmain  12756  dfgcd2  12772  pw2dvdslemn  12924  oddprmdvds  13114  sgrpidmndm  13713  srgmulgass  14270  ringinvnzdiv  14331  lmodvsmmulgdi  14635  topbas  15094  cnplimclemr  15696  limccnp2lem  15703  gausslemma2dlem3  16099  upgriswlkdc  16518  clwwlkccatlem  16558  umgr2cwwk2dif  16582  clwwlknonex2  16597  depindlem2  16665  depindlem3  16666  nninfalllem1  16959  nninfsellemdc  16961  nninfsellemqall  16966  isomninnlem  16987  trirec0  17001  ismkvnnlem  17010