MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expr Structured version   Unicode version

Theorem expr 615
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
expr.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
expr  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 605 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 429 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  reximddv  2925  rexlimdvaa  2938  disjxiun  4387  wereu2  4815  suppssOLD  5935  fcof1  6090  knatar  6147  riota5f  6176  ovmpt2df  6322  suppss2OLD  6415  extmptsuppeq  6813  suppss  6819  suppss2  6823  smoord  6926  tfrlem9a  6945  oaass  7100  oelimcl  7139  oaabs2  7184  swoso  7232  eceqoveq  7305  domdifsn  7494  domunsncan  7511  omxpenlem  7512  enfixsn  7520  mapdom2  7582  frfi  7658  fofinf1o  7693  finsschain  7719  elfiun  7781  marypha1lem  7784  eqsupd  7808  ordiso2  7830  ordtypelem6  7838  ordtypelem7  7839  ordtypelem10  7842  oismo  7855  wemapsolem  7865  brwdom2  7889  wdomtr  7891  unwdomg  7900  xpwdomg  7901  unxpwdom2  7904  cantnfval2  7978  cantnfle  7980  cantnflem1  7998  cantnf  8002  cantnfval2OLD  8008  cantnfleOLD  8010  cantnflem1OLD  8021  cantnfOLD  8024  r1ordg  8086  tcrank  8192  carddomi2  8241  harval2  8268  infxpenlem  8281  infxpenc2lem2  8287  infxpenc2lem2OLD  8291  fseqenlem1  8295  dfac8clem  8303  acndom2  8325  infpwfien  8333  iunfictbso  8385  dfac12lem3  8415  infxp  8485  coflim  8531  cofsmo  8539  coftr  8543  sornom  8547  infpssrlem4  8576  enfin2i  8591  fin23lem26  8595  fin23lem27  8598  fin23lem36  8618  fin23lem40  8621  isf32lem5  8627  isf34lem4  8647  isfin1-3  8656  fin1a2lem10  8679  fin1a2lem13  8682  fin1a2s  8684  hsmexlem4  8699  ttukeylem5  8783  ttukeylem6  8784  ttukeylem7  8785  alephval2  8837  gchor  8895  fpwwe2lem7  8904  fpwwe2lem12  8909  fpwwe2  8911  pwfseqlem4a  8929  pwfseqlem4  8930  winalim2  8964  gchina  8967  inar1  9043  nqereq  9205  prlem934  9303  prlem936  9317  supsrlem  9379  axpre-sup  9437  dedekind  9634  dedekindle  9635  prodge0  10277  mulge0b  10300  supmul1  10396  un0addcl  10714  un0mulcl  10715  uzwo3  11049  qbtwnre  11270  xlemul1a  11352  seqcl2  11925  seqfveq2  11929  seqshft2  11933  monoord  11937  seqsplit  11940  seqf1olem1  11946  seqid2  11953  seqhomo  11954  expnegz  11999  expcan  12017  ltexp2  12018  discr  12102  bcval5  12195  hashbc  12308  hashf1lem2  12311  seqcoll  12318  seqcoll2  12319  wrdind  12473  wrd2ind  12474  cau3lem  12944  ello1d  13103  lo1bdd2  13104  rlimclim  13126  climrlim2  13127  rlimdm  13131  rlimcn1  13168  reccn2  13176  rlimsqzlem  13228  lo1le  13231  caucvgrlem  13252  caurcvg2  13257  summolem2  13295  zsum  13297  fsum  13299  fsumf1o  13302  sumss  13303  fsumss  13304  fsumcl2lem  13310  fsumadd  13317  fsumcom2  13343  fsum0diag2  13352  fsummulc2  13353  fsumconst  13359  fsumrelem  13372  fsumrlim  13376  fsumo1  13377  divrcnv  13417  geomulcvg  13438  mertenslem2  13447  ruclem8  13621  dvds0lem  13645  dvdsnegb  13652  dvdssub2  13672  bitsf1  13744  bitsshft  13773  bezoutlem3  13826  bezoutlem4  13827  isprm2lem  13872  isprm6  13897  isprm5  13900  modprminv  13972  modprminveq  13973  reumodprminv  13974  pcqmul  14022  pcqcl  14025  pcxcl  14029  pc2dvds  14047  pcadd  14053  pcmpt  14056  pockthg  14069  infpnlem1  14073  prmreclem5  14083  vdwlem2  14145  vdwlem9  14152  vdwlem10  14153  vdwlem12  14155  ramub  14176  0ram  14183  ramub1lem2  14190  ramub1  14191  ramcl  14192  mreexexd  14688  acsfn2  14703  iscatd  14713  catpropd  14750  setcmon  15057  drsdirfi  15210  pleval2i  15236  psss  15486  mhmeql  15594  gsumvallem1  15602  frmdss2  15643  frmdup3  15646  grprcan  15673  mulgnn0ass  15758  isnsg3  15817  ghmpreima  15870  ghmeql  15871  gaorber  15928  f1omvdco2  16056  psgnunilem1  16101  psgnunilem2  16103  oddvds  16154  gexdvds  16187  sylow1lem1  16201  odcau  16207  pgpssslw  16217  sylow2alem2  16221  sylow2blem3  16225  fislw  16228  sylow2  16229  lsmmod  16276  efgredlem  16348  frgpup3  16379  gexex  16439  gsumval3OLD  16486  gsumval3  16489  gsumzres  16492  gsumzcl2  16493  gsumzf1o  16495  gsumzresOLD  16496  gsumzclOLD  16497  gsumzf1oOLD  16498  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumconst  16532  gsumzmhm  16535  gsumzmhmOLD  16536  gsumzoppg  16545  gsumzoppgOLD  16546  gsum2d2lem  16570  ablfac1eulem  16678  pgpfac1lem5  16685  ablfaclem3  16693  issubdrg  16996  lss1d  17150  lmhmeql  17242  lspextmo  17243  lspsnat  17332  lsppratlem6  17339  islbs3  17342  lbsextlem4  17348  lidl1el  17406  mvrf1  17605  mplsubglem  17617  mpllsslem  17618  mplsubglemOLD  17619  mpllsslemOLD  17620  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  cnsubrg  17982  gsumfsum  17988  prmirredlem  18026  prmirredlemOLD  18029  znidomb  18103  frgpcyg  18115  cssmre  18227  dsmmsubg  18277  dsmmlss  18278  frlmsslsp  18332  frlmsslspOLD  18333  lindff1  18358  lindfrn  18359  mdetdiaglem  18520  mdetunilem7  18540  mdetunilem8  18541  mdetunilem9  18542  en2top  18706  toponmre  18813  topssnei  18844  innei  18845  clslp  18868  restcls  18901  restntr  18902  ordtrest2lem  18923  cnpco  18987  cncls2  18993  cncnpi  18998  cncnp  19000  cnconst2  19003  cnpdis  19013  lmcnp  19024  cnhaus  19074  nrmsep  19077  regsep2  19096  isreg2  19097  cncmp  19111  tgcmp  19120  sscmp  19124  cmpfi  19127  cnconn  19142  iunconlem  19147  clscon  19150  1stcfb  19165  1stcrest  19173  2ndcctbss  19175  2ndcdisj  19176  1stcelcls  19181  1stccnp  19182  restnlly  19202  cldllycmp  19215  lly1stc  19216  dislly  19217  kgentopon  19227  kgenidm  19236  1stckgenlem  19242  kgencn3  19247  ptpjpre1  19260  ptbasin  19266  txcls  19293  tx2cn  19299  ptpjcn  19300  ptclsg  19304  ptcnp  19311  txdis  19321  txlly  19325  txnlly  19326  pthaus  19327  txtube  19329  txcmplem1  19330  txcmplem2  19331  txcmp  19332  txhaus  19336  txkgen  19341  xkohaus  19342  xkococnlem  19348  xkococn  19349  txcon  19378  qtopeu  19405  qtoprest  19406  regr1lem2  19429  kqreglem1  19430  cmphaushmeo  19489  xkocnv  19503  fgabs  19568  filuni  19574  trufil  19599  ufileu  19608  filufint  19609  fin1aufil  19621  elfm2  19637  rnelfmlem  19641  fmfnfmlem2  19644  fmfnfmlem4  19646  fmufil  19648  flimopn  19664  fbflim2  19666  hausflimi  19669  hausflim  19670  flimcf  19671  flimclslem  19673  flimsncls  19675  hauspwpwf1  19676  cnpflfi  19688  fclsnei  19708  fclscf  19714  flimfnfcls  19717  fclscmp  19719  ufilcmp  19721  fcfnei  19724  cnpfcf  19730  alexsublem  19732  alexsub  19733  alexsubALTlem2  19736  alexsubALTlem3  19737  alexsubALTlem4  19738  ptcmplem3  19742  ptcmplem4  19743  ptcmplem5  19744  symgtgp  19788  tgpconcompeqg  19798  tgpconcomp  19799  ghmcnp  19801  tgpt0  19805  divstgplem  19807  haustsms2  19823  tsmsgsum  19825  tsmsgsumOLD  19828  tsmsresOLD  19833  tsmsres  19834  tsmsxp  19845  imasdsf1olem  20064  xbln0  20105  blssps  20115  blss  20116  neibl  20192  blcld  20196  metss  20199  metequiv2  20201  met1stc  20212  metrest  20215  prdsxmslem2  20220  metcnp3  20231  nrmmetd  20283  nlmvscnlem1  20383  nrginvrcnlem  20387  nmoleub  20426  icccmplem2  20516  icccmp  20518  reconnlem2  20520  xrge0tsms  20527  metdstri  20543  metdseq0  20546  metdscn  20548  cnmpt2pc  20616  cnheibor  20643  lebnumlem3  20651  pcoval2  20704  pcopt  20710  nmoleub2lem  20785  nmhmcn  20791  ipcnlem1  20873  cfilfcls  20901  cmetcaulem  20915  iscmet3lem2  20919  iscmet3  20920  equivcau  20927  caubl  20934  lmcau  20939  bcthlem2  20952  bcthlem3  20953  bcthlem4  20954  bcthlem5  20955  ivthlem2  21052  ivthlem3  21053  ovoliunlem2  21102  ovolicc2lem2  21117  ovolicc2lem3  21118  ovolicc2lem5  21120  ovolicc2  21121  ismbl2  21126  nulmbl  21133  nulmbl2  21134  unmbl  21135  shftmbl  21136  voliunlem3  21149  volsup  21153  ioombl1lem4  21158  ioombl1  21159  icombl  21161  ioombl  21162  uniioombl  21185  opnmbllem  21197  volivth  21203  vitali  21209  ismbf3d  21248  mbflimsup  21260  i1fadd  21289  itg1addlem4  21293  itg2le  21333  itg2seq  21336  itg2lea  21338  itg2splitlem  21342  itg2split  21343  itg2mono  21347  itg2gt0  21354  itg2cnlem2  21356  itgss  21405  itgfsum  21420  itgcn  21436  ellimc3  21470  limcco  21484  limciun  21485  dvnres  21521  dvnfre  21542  rolle  21578  c1liplem1  21584  dvivth  21598  dvne0  21599  lhop1lem  21601  lhop1  21602  lhop  21604  dvcnvrelem1  21605  dvfsumrlim  21619  dvfsum2  21622  ftc1a  21625  ftc1lem6  21629  itgsubst  21637  tdeglem4  21645  mdegaddle  21661  mdegvscale  21662  mdegmullem  21665  deg1tmle  21705  ply1divex  21724  dvdsq1p  21748  fta1g  21755  fta1b  21757  plyco0  21776  coeeulem  21808  dgrlem  21813  plyco  21825  coemullem  21833  dgreq0  21848  dgrco  21858  plydivex  21879  quotcan  21891  aannenlem1  21910  aalioulem2  21915  aalioulem3  21916  taylthlem1  21954  ulmbdd  21979  ulmdvlem3  21983  itgulm  21989  radcnvlt1  21999  psercnlem1  22006  abelthlem2  22013  abelthlem8  22020  logcnlem5  22207  efopn  22219  cxpmul2z  22252  cxpcn3lem  22301  cxpeq  22311  xrlimcnp  22478  cxplim  22481  o1cxp  22484  cxploglim  22487  scvxcvx  22495  jensen  22498  ftalem1  22526  ftalem2  22527  fta  22533  basellem3  22536  isppw2  22569  ppinprm  22606  chtnprm  22608  dvdsmulf1o  22650  chtublem  22666  perfectlem2  22685  dchrfi  22710  dchrptlem1  22719  dchrptlem2  22720  dchrptlem3  22721  dchrsum2  22723  bposlem1  22739  bposlem3  22741  2sqlem5  22823  2sqlem6  22824  2sqlem8  22827  2sqlem10  22829  2sqb  22833  chebbnd1lem1  22834  chtppilimlem2  22839  dchrisum0flb  22875  dchrisum0fno1  22876  dchrisum0  22885  pntrsumbnd2  22932  pntpbnd1  22951  pntpbnd2  22952  pntlemp  22975  pnt3  22977  qabvle  22990  ostth2lem2  22999  ostth3  23003  ostth  23004  colinearalglem4  23290  axcontlem10  23354  umgraex  23392  eupai  23723  isgrp2d  23857  ghgrp  23990  ghablo  23991  smcnlem  24227  ubthlem1  24406  ubthlem3  24408  htthlem  24454  pjhthlem2  24930  5oalem6  25197  leopmuli  25672  pjnormssi  25707  pjclem4  25738  pj3si  25746  hatomistici  25901  sumdmdlem  25957  suppss2f  26088  xrge0tsmsd  26387  isarchiofld  26419  ordtrest2NEWlem  26486  qqhf  26549  eulerpartlemb  26885  ballotlemfc0  27009  ballotlemfcc  27010  sgn3da  27058  subfacp1lem5  27206  erdszelem7  27219  erdszelem11  27223  pconcon  27254  txpcon  27255  conpcon  27258  sconpi1  27262  txscon  27264  cvxscon  27266  cvmopnlem  27301  cvmfolem  27302  cvmliftmolem2  27305  cvmliftlem7  27314  cvmliftlem10  27317  cvmliftlem15  27321  cvmlift2lem10  27335  cvmlift3lem4  27345  cvmlift3lem8  27349  prodmolem2  27582  zprod  27584  fprod  27588  fprodf1o  27593  prodss  27594  fprodss  27595  fprodcl2lem  27597  fprodmul  27605  fproddiv  27606  fprodconst  27623  fprodn0  27624  fprodcom2  27629  wzel  27895  wsuclem  27896  nofulllem4  27980  btwnouttr2  28187  cgrxfr  28220  btwnxfr  28221  brcolinear  28224  lineext  28241  btwnconn1lem13  28264  midofsegid  28269  segcon2  28270  brsegle  28273  seglecgr12im  28275  segletr  28279  colinbtwnle  28283  broutsideof2  28287  btwnoutside  28290  broutsideof3  28291  outsideoftr  28294  outsideofeq  28295  outsideofeu  28296  outsidele  28297  lineunray  28312  lineelsb2  28313  linethru  28318  wl-sbcom2d-lem1  28523  finixpnum  28552  supaddc  28555  heicant  28564  opnmbllem0  28565  mblfinlem3  28568  ismblfin  28570  ovoliunnfl  28571  voliunnfl  28573  volsupnfl  28574  itg2addnclem  28581  itg2addnclem3  28583  ftc1cnnc  28604  finminlem  28651  nn0prpwlem  28655  locfincmp  28714  comppfsc  28717  neibastop2lem  28719  neibastop2  28720  neibastop3  28721  topjoin  28724  tailfb  28736  sdclem2  28776  fdc  28779  istotbnd3  28808  isbnd2  28820  isbnd3  28821  prdsbnd  28830  cntotbnd  28833  heibor1lem  28846  heibor1  28847  heiborlem10  28857  rrncmslem  28869  ghomco  28886  1idl  28964  unichnidl  28969  prtlem10  29148  prtlem18  29160  isnacs3  29184  nacsfix  29186  fnwe2lem2  29542  kelac1  29554  unxpwdom3  29586  hbtlem5  29622  hbt  29624  dgraa0p  29644  hashgcdeq  29704  rlimdmafv  30221  numclwwlkovf2ex  30817  gsummoncoe1  30985  mat1dimcrng  31027  lindslinindsimp2  31104  cpmatacl  31179  cpmatmcllem  31181  mp2pm2mplem4  31264  atlatmstc  33270  cvrexchlem  33369  paddasslem14  33783  pexmidlem5N  33924  cdleme29ex  34324  cdlemefr29exN  34352  cdleme32fva  34387  diarnN  35080  dihlsscpre  35185
  Copyright terms: Public domain W3C validator