MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expr 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
Assertion
Ref Expression
expr

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3
21exp32 605 . 2
32imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  reximddv  2933  rexlimdvaa  2950  disjxiun  4449  wereu2  4881  suppssOLD  6020  fcof1  6190  knatar  6253  riota5f  6282  ovmpt2df  6434  suppss2OLD  6530  extmptsuppeq  6943  suppss  6949  suppss2  6953  smoord  7055  tfrlem9a  7074  oaass  7229  oelimcl  7268  oaabs2  7313  swoso  7361  eceqoveq  7435  domdifsn  7620  domunsncan  7637  omxpenlem  7638  enfixsn  7646  mapdom2  7708  frfi  7785  fofinf1o  7821  finsschain  7847  elfiun  7910  marypha1lem  7913  eqsupd  7937  ordiso2  7961  ordtypelem6  7969  ordtypelem7  7970  ordtypelem10  7973  oismo  7986  wemapsolem  7996  brwdom2  8020  wdomtr  8022  unwdomg  8031  xpwdomg  8032  unxpwdom2  8035  cantnfval2  8109  cantnfle  8111  cantnflem1  8129  cantnf  8133  cantnfval2OLD  8139  cantnfleOLD  8141  cantnflem1OLD  8152  cantnfOLD  8155  r1ordg  8217  tcrank  8323  carddomi2  8372  harval2  8399  infxpenlem  8412  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  fseqenlem1  8426  dfac8clem  8434  acndom2  8456  infpwfien  8464  iunfictbso  8516  dfac12lem3  8546  infxp  8616  coflim  8662  cofsmo  8670  coftr  8674  sornom  8678  infpssrlem4  8707  enfin2i  8722  fin23lem26  8726  fin23lem27  8729  fin23lem36  8749  fin23lem40  8752  isf32lem5  8758  isf34lem4  8778  isfin1-3  8787  fin1a2lem10  8810  fin1a2lem13  8813  fin1a2s  8815  hsmexlem4  8830  ttukeylem5  8914  ttukeylem6  8915  ttukeylem7  8916  alephval2  8968  gchor  9026  fpwwe2lem7  9035  fpwwe2lem12  9040  fpwwe2  9042  pwfseqlem4a  9060  pwfseqlem4  9061  winalim2  9095  gchina  9098  inar1  9174  nqereq  9334  prlem934  9432  prlem936  9446  addsrmo  9471  mulsrmo  9472  supsrlem  9509  axpre-sup  9567  dedekind  9765  dedekindle  9766  prodge0  10414  mulge0b  10437  supmul1  10533  un0addcl  10854  un0mulcl  10855  uzwo3  11206  qbtwnre  11427  xlemul1a  11509  seqcl2  12125  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqf1olem1  12146  seqid2  12153  seqhomo  12154  expnegz  12200  expcan  12218  ltexp2  12219  discr  12303  bcval5  12396  hashbc  12502  hashf1lem2  12505  seqcoll  12512  seqcoll2  12513  wrdind  12702  wrd2ind  12703  cau3lem  13187  ello1d  13346  lo1bdd2  13347  rlimclim  13369  climrlim2  13370  rlimdm  13374  rlimcn1  13411  reccn2  13419  rlimsqzlem  13471  lo1le  13474  caucvgrlem  13495  caurcvg2  13500  summolem2  13538  zsum  13540  fsum  13542  fsumf1o  13545  sumss  13546  fsumss  13547  fsumcl2lem  13553  fsumadd  13561  fsumcom2  13589  fsum0diag2  13598  fsummulc2  13599  fsumconst  13605  fsumrelem  13621  fsumrlim  13625  fsumo1  13626  divrcnv  13664  geomulcvg  13685  mertenslem2  13694  prodmolem2  13742  zprod  13744  fprod  13748  fprodf1o  13753  prodss  13754  fprodss  13755  fprodcl2lem  13757  fprodmul  13765  fproddiv  13766  fprodconst  13782  fprodn0  13783  fprodcom2  13788  ruclem8  13970  dvds0lem  13994  dvdsnegb  14001  dvdssub2  14023  bitsf1  14096  bitsshft  14125  bezoutlem3  14178  bezoutlem4  14179  isprm2lem  14224  isprm6  14250  isprm5  14253  modprminv  14326  modprminveq  14327  reumodprminv  14329  pcqmul  14377  pcqcl  14380  pcxcl  14384  pc2dvds  14402  pcadd  14408  pcmpt  14411  pockthg  14424  infpnlem1  14428  prmreclem5  14438  vdwlem2  14500  vdwlem9  14507  vdwlem10  14508  vdwlem12  14510  ramub  14531  0ram  14538  ramub1lem2  14545  ramub1  14546  ramcl  14547  mreexexd  15045  acsfn2  15060  iscatd  15070  catpropd  15104  setcmon  15414  pleval2i  15594  psss  15844  mgmidsssn0  15896  mhmeql  15995  frmdss2  16031  frmdup3  16035  grprcan  16083  mulgnn0ass  16171  isnsg3  16235  ghmpreima  16288  ghmeql  16289  gaorber  16346  f1omvdco2  16473  psgnunilem1  16518  psgnunilem2  16520  oddvds  16571  gexdvds  16604  sylow1lem1  16618  odcau  16624  pgpssslw  16634  sylow2alem2  16638  sylow2blem3  16642  fislw  16645  lsmmod  16693  efgredlem  16765  frgpup3  16796  gsumval3OLD  16908  gsumval3  16911  gsumzres  16914  gsumzcl2  16915  gsumzf1o  16917  gsumzresOLD  16918  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  gsum2d2lem  17001  ablfac1eulem  17123  pgpfac1lem5  17130  ablfaclem3  17138  issubdrg  17454  lss1d  17609  lmhmeql  17701  lspextmo  17702  lspsnat  17791  lsppratlem6  17798  islbs3  17801  lbsextlem4  17807  lidl1el  17866  mvrf1  18081  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  gsummoncoe1  18346  cnsubrg  18478  gsumfsum  18484  prmirredlem  18523  prmirredlemOLD  18526  znidomb  18600  frgpcyg  18612  cssmre  18724  dsmmsubg  18774  dsmmlss  18775  frlmsslsp  18829  frlmsslspOLD  18830  lindff1  18855  lindfrn  18856  mat1dimcrng  18979  mdetdiaglem  19100  mdetunilem7  19120  mdetunilem8  19121  mdetunilem9  19122  cpmatacl  19217  cpmatmcllem  19219  mp2pm2mplem4  19310  en2top  19487  toponmre  19594  topssnei  19625  innei  19626  clslp  19649  restcls  19682  restntr  19683  ordtrest2lem  19704  cnpco  19768  cncls2  19774  cncnpi  19779  cncnp  19781  cnconst2  19784  cnpdis  19794  lmcnp  19805  cnhaus  19855  isreg2  19878  cncmp  19892  tgcmp  19901  sscmp  19905  cmpfi  19908  cnconn  19923  iunconlem  19928  clscon  19931  1stcfb  19946  1stcrest  19954  2ndcctbss  19956  2ndcdisj  19957  1stcelcls  19962  1stccnp  19963  restnlly  19983  cldllycmp  19996  lly1stc  19997  dislly  19998  locfincmp  20027  comppfsc  20033  kgentopon  20039  kgenidm  20048  1stckgenlem  20054  kgencn3  20059  ptpjpre1  20072  ptbasin  20078  txcls  20105  tx2cn  20111  ptpjcn  20112  ptclsg  20116  ptcnp  20123  txdis  20133  txlly  20137  txnlly  20138  pthaus  20139  txtube  20141  txcmplem1  20142  txcmplem2  20143  txcmp  20144  txhaus  20148  txkgen  20153  xkohaus  20154  xkococnlem  20160  xkococn  20161  txcon  20190  qtopeu  20217  qtoprest  20218  regr1lem2  20241  kqreglem1  20242  cmphaushmeo  20301  xkocnv  20315  fgabs  20380  filuni  20386  trufil  20411  ufileu  20420  filufint  20421  fin1aufil  20433  elfm2  20449  rnelfmlem  20453  fmfnfmlem2  20456  fmfnfmlem4  20458  fmufil  20460  flimopn  20476  fbflim2  20478  hausflimi  20481  hausflim  20482  flimcf  20483  flimclslem  20485  flimsncls  20487  hauspwpwf1  20488  cnpflfi  20500  fclsnei  20520  fclscf  20526  flimfnfcls  20529  fclscmp  20531  ufilcmp  20533  fcfnei  20536  cnpfcf  20542  alexsublem  20544  alexsub  20545  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem3  20554  ptcmplem4  20555  ptcmplem5  20556  symgtgp  20600  tgpconcompeqg  20610  tgpconcomp  20611  ghmcnp  20613  tgpt0  20617  qustgplem  20619  haustsms2  20635  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsxp  20657  imasdsf1olem  20876  xbln0  20917  blssps  20927  blss  20928  neibl  21004  blcld  21008  metss  21011  metequiv2  21013  met1stc  21024  metrest  21027  prdsxmslem2  21032  metcnp3  21043  nrmmetd  21095  nlmvscnlem1  21195  nrginvrcnlem  21199  nmoleub  21238  icccmplem2  21328  icccmp  21330  reconnlem2  21332  xrge0tsms  21339  metdstri  21355  metdseq0  21358  metdscn  21360  cnmpt2pc  21428  lebnumlem3  21463  pcoval2  21516  pcopt  21522  nmoleub2lem  21597  nmhmcn  21603  ipcnlem1  21685  cfilfcls  21713  cmetcaulem  21727  iscmet3lem2  21731  iscmet3  21732  equivcau  21739  caubl  21746  bcthlem2  21764  bcthlem3  21765  bcthlem4  21766  bcthlem5  21767  ivthlem2  21864  ivthlem3  21865  ovoliunlem2  21914  ovolicc2lem2  21929  ovolicc2lem3  21930  ovolicc2lem5  21932  ovolicc2  21933  ismbl2  21938  nulmbl  21946  nulmbl2  21947  unmbl  21948  shftmbl  21949  voliunlem3  21962  volsup  21966  ioombl1lem4  21971  ioombl1  21972  icombl  21974  ioombl  21975  uniioombl  21998  opnmbllem  22010  volivth  22016  vitali  22022  mbflimsup  22073  i1fadd  22102  itg1addlem4  22106  itg2le  22146  itg2seq  22149  itg2lea  22151  itg2splitlem  22155  itg2split  22156  itg2mono  22160  itg2gt0  22167  itg2cnlem2  22169  itgss  22218  itgfsum  22233  itgcn  22249  ellimc3  22283  limcco  22297  limciun  22298  dvnres  22334  dvnfre  22355  rolle  22391  c1liplem1  22397  dvivth  22411  dvne0  22412  lhop1lem  22414  lhop1  22415  lhop  22417  dvcnvrelem1  22418  dvfsumrlim  22432  dvfsum2  22435  ftc1a  22438  ftc1lem6  22442  itgsubst  22450  tdeglem4  22458  mdegaddle  22474  mdegvscale  22475  mdegmullem  22478  deg1tmle  22518  ply1divex  22537  dvdsq1p  22561  fta1g  22568  fta1b  22570  plyco0  22589  coeeulem  22621  dgrlem  22626  plyco  22638  coemullem  22647  dgreq0  22662  dgrco  22672  plydivex  22693  quotcan  22705  aannenlem1  22724  aalioulem2  22729  aalioulem3  22730  taylthlem1  22768  ulmbdd  22793  itgulm  22803  radcnvlt1  22813  psercnlem1  22820  abelthlem2  22827  abelthlem8  22834  logcnlem5  23027  efopn  23039  cxpmul2z  23072  cxpcn3lem  23121  cxpeq  23131  xrlimcnp  23298  cxplim  23301  o1cxp  23304  cxploglim  23307  scvxcvx  23315  jensen  23318  ftalem1  23346  ftalem2  23347  fta  23353  basellem3  23356  isppw2  23389  ppinprm  23426  chtnprm  23428  dvdsmulf1o  23470  chtublem  23486  perfectlem2  23505  dchrfi  23530  dchrptlem1  23539  dchrptlem2  23540  dchrptlem3  23541  dchrsum2  23543  bposlem1  23559  bposlem3  23561  2sqlem5  23643  2sqlem6  23644  2sqlem8  23647  2sqlem10  23649  2sqb  23653  chebbnd1lem1  23654  chtppilimlem2  23659  dchrisum0flb  23695  dchrisum0fno1  23696  dchrisum0  23705  pntrsumbnd2  23752  pntpbnd1  23771  pntpbnd2  23772  pntlemp  23795  pnt3  23797  qabvle  23810  ostth2lem2  23819  ostth3  23823  ostth  23824  colinearalglem4  24212  axcontlem10  24276  umgraex  24323  eupai  24967  numclwwlkovf2ex  25086  isgrp2d  25237  ghgrpOLD  25370  ghabloOLD  25371  smcnlem  25607  ubthlem1  25786  ubthlem3  25788  htthlem  25834  5oalem6  26577  leopmuli  27052  pjnormssi  27087  pjclem4  27118  pj3si  27126  hatomistici  27281  sumdmdlem  27337  suppss2f  27477  xrge0tsmsd  27775  isarchiofld  27807  ordtrest2NEWlem  27904  qqhf  27967  eulerpartlemb  28307  ballotlemfc0  28431  ballotlemfcc  28432  sgn3da  28480  subfacp1lem5  28628  erdszelem7  28641  erdszelem11  28645  pconcon  28676  txpcon  28677  conpcon  28680  sconpi1  28684  txscon  28686  cvxscon  28688  cvmopnlem  28723  cvmfolem  28724  cvmliftmolem2  28727  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift2lem10  28757  cvmlift3lem4  28767  cvmlift3lem8  28771  msubff1  28916  wzel  29380  wsuclem  29381  nofulllem4  29465  btwnouttr2  29672  cgrxfr  29705  btwnxfr  29706  brcolinear  29709  lineext  29726  btwnconn1lem13  29749  midofsegid  29754  segcon2  29755  brsegle  29758  seglecgr12im  29760  segletr  29764  colinbtwnle  29768  broutsideof2  29772  btwnoutside  29775  broutsideof3  29776  outsideoftr  29779  outsideofeq  29780  outsideofeu  29781  outsidele  29782  lineunray  29797  lineelsb2  29798  linethru  29803  wl-sbcom2d-lem1  30009  finixpnum  30038  supaddc  30041  heicant  30049  opnmbllem0  30050  mblfinlem3  30053  ismblfin  30055  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  itg2addnclem  30066  itg2addnclem3  30068  ftc1cnnc  30089  finminlem  30136  nn0prpwlem  30140  neibastop2lem  30178  neibastop2  30179  neibastop3  30180  topjoin  30183  tailfb  30195  sdclem2  30235  fdc  30238  istotbnd3  30267  isbnd2  30279  isbnd3  30280  prdsbnd  30289  cntotbnd  30292  heibor1lem  30305  heibor1  30306  heiborlem10  30316  rrncmslem  30328  ghomco  30345  1idl  30423  unichnidl  30428  prtlem10  30606  prtlem18  30618  isnacs3  30642  fnwe2lem2  30997  kelac1  31009  hbtlem5  31077  hbt  31079  dgraa0p  31098  hashgcdeq  31158  rlimdmafv  32262  mgmhmeql  32491  lindslinindsimp2  33064  atlatmstc  35044  cvrexchlem  35143  paddasslem14  35557  pexmidlem5N  35698  cdleme29ex  36100  cdlemefr29exN  36128  cdleme32fva  36163  diarnN  36856  dihlsscpre  36961
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
  Copyright terms: Public domain W3C validator