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  864  3impa  1220  exp516  1253  rexlimdva2  2653  r19.29af2  2673  disjiun  4083  mpteqb  5738  dffo3  5795  fconstfvm  5873  fliftfun  5940  tfrlem1  6477  tfrlem9  6488  tfr1onlemaccex  6517  tfrcllemaccex  6530  tfrcl  6533  nnsucsssuc  6663  nnaordex  6699  diffifi  7086  fidcenumlemrk  7156  fidcenumlemr  7157  nninfninc  7325  nnnninfeq  7330  nnnninfeq2  7331  exmidontriimlem4  7442  exmidontriim  7443  prarloclemup  7718  genpcdl  7742  genpcuu  7743  negf1o  8564  recexap  8836  zaddcllemneg  9521  zdiv  9571  uzaddcl  9823  fz0fzelfz0  10365  fz0fzdiffz0  10368  elfzmlbp  10370  difelfzle  10372  fzo1fzo0n0  10426  elincfzoext  10442  ssfzo12bi  10474  exfzdc  10490  zsupcllemstep  10493  modfzo0difsn  10661  frecuzrdgg  10682  seq3val  10726  seqvalcd  10727  seqf1og  10787  exp3vallem  10806  expcllem  10816  expap0  10835  mulexp  10844  swrdnd  11247  swrdswrdlem  11292  swrdswrd  11293  pfxccat3  11322  reuccatpfxs1  11335  cjexp  11474  absexp  11660  fimaxre2  11808  summodc  11965  fsum2d  12017  modfsummod  12040  binom  12066  clim2prod  12121  fprod2d  12205  efexp  12264  demoivreALT  12356  divconjdvds  12431  addmodlteqALT  12441  divalglemeunn  12503  divalglemeuneg  12505  bezoutlemstep  12589  bezoutlemmain  12590  dfgcd2  12606  pw2dvdslemn  12758  oddprmdvds  12948  sgrpidmndm  13524  gsumfzz  13599  srgmulgass  14024  ringinvnzdiv  14085  lmodvsmmulgdi  14359  topbas  14818  cnplimclemr  15420  limccnp2lem  15427  gausslemma2dlem3  15819  upgriswlkdc  16238  clwwlkccatlem  16278  umgr2cwwk2dif  16302  clwwlknonex2  16317  depindlem2  16385  depindlem3  16386  nninfalllem1  16669  nninfsellemdc  16671  nninfsellemqall  16676  isomninnlem  16693  trirec0  16707  ismkvnnlem  16716