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  2937  rexlimdvaa  2951  disjxiun  4406  wereu2  4834  suppssOLD  5959  fcof1  6116  knatar  6179  riota5f  6208  ovmpt2df  6355  suppss2OLD  6448  extmptsuppeq  6847  suppss  6853  suppss2  6857  smoord  6960  tfrlem9a  6979  oaass  7134  oelimcl  7173  oaabs2  7218  swoso  7266  eceqoveq  7339  domdifsn  7528  domunsncan  7545  omxpenlem  7546  enfixsn  7554  mapdom2  7616  frfi  7692  fofinf1o  7727  finsschain  7753  elfiun  7816  marypha1lem  7819  eqsupd  7843  ordiso2  7866  ordtypelem6  7874  ordtypelem7  7875  ordtypelem10  7878  oismo  7891  wemapsolem  7901  brwdom2  7925  wdomtr  7927  unwdomg  7936  xpwdomg  7937  unxpwdom2  7940  cantnfval2  8014  cantnfle  8016  cantnflem1  8034  cantnf  8038  cantnfval2OLD  8044  cantnfleOLD  8046  cantnflem1OLD  8057  cantnfOLD  8060  r1ordg  8122  tcrank  8228  carddomi2  8277  harval2  8304  infxpenlem  8317  infxpenc2lem2  8323  infxpenc2lem2OLD  8327  fseqenlem1  8331  dfac8clem  8339  acndom2  8361  infpwfien  8369  iunfictbso  8421  dfac12lem3  8451  infxp  8521  coflim  8567  cofsmo  8575  coftr  8579  sornom  8583  infpssrlem4  8612  enfin2i  8627  fin23lem26  8631  fin23lem27  8634  fin23lem36  8654  fin23lem40  8657  isf32lem5  8663  isf34lem4  8683  isfin1-3  8692  fin1a2lem10  8715  fin1a2lem13  8718  fin1a2s  8720  hsmexlem4  8735  ttukeylem5  8819  ttukeylem6  8820  ttukeylem7  8821  alephval2  8873  gchor  8931  fpwwe2lem7  8940  fpwwe2lem12  8945  fpwwe2  8947  pwfseqlem4a  8965  pwfseqlem4  8966  winalim2  9000  gchina  9003  inar1  9079  nqereq  9241  prlem934  9339  prlem936  9353  supsrlem  9415  axpre-sup  9473  dedekind  9670  dedekindle  9671  prodge0  10313  mulge0b  10336  supmul1  10432  un0addcl  10751  un0mulcl  10752  uzwo3  11087  qbtwnre  11308  xlemul1a  11390  seqcl2  11981  seqfveq2  11985  seqshft2  11989  monoord  11993  seqsplit  11996  seqf1olem1  12002  seqid2  12009  seqhomo  12010  expnegz  12055  expcan  12073  ltexp2  12074  discr  12158  bcval5  12251  hashbc  12364  hashf1lem2  12367  seqcoll  12374  seqcoll2  12375  wrdind  12529  wrd2ind  12530  cau3lem  13000  ello1d  13159  lo1bdd2  13160  rlimclim  13182  climrlim2  13183  rlimdm  13187  rlimcn1  13224  reccn2  13232  rlimsqzlem  13284  lo1le  13287  caucvgrlem  13308  caurcvg2  13313  summolem2  13351  zsum  13353  fsum  13355  fsumf1o  13358  sumss  13359  fsumss  13360  fsumcl2lem  13366  fsumadd  13373  fsumcom2  13399  fsum0diag2  13408  fsummulc2  13409  fsumconst  13415  fsumrelem  13428  fsumrlim  13432  fsumo1  13433  divrcnv  13473  geomulcvg  13494  mertenslem2  13503  ruclem8  13677  dvds0lem  13701  dvdsnegb  13708  dvdssub2  13728  bitsf1  13800  bitsshft  13829  bezoutlem3  13882  bezoutlem4  13883  isprm2lem  13928  isprm6  13953  isprm5  13956  modprminv  14028  modprminveq  14029  reumodprminv  14030  pcqmul  14078  pcqcl  14081  pcxcl  14085  pc2dvds  14103  pcadd  14109  pcmpt  14112  pockthg  14125  infpnlem1  14129  prmreclem5  14139  vdwlem2  14201  vdwlem9  14208  vdwlem10  14209  vdwlem12  14211  ramub  14232  0ram  14239  ramub1lem2  14246  ramub1  14247  ramcl  14248  mreexexd  14745  acsfn2  14760  iscatd  14770  catpropd  14807  setcmon  15114  drsdirfi  15267  pleval2i  15293  psss  15543  mhmeql  15651  gsumvallem1  15659  frmdss2  15700  frmdup3  15703  grprcan  15730  mulgnn0ass  15815  isnsg3  15874  ghmpreima  15927  ghmeql  15928  gaorber  15985  f1omvdco2  16113  psgnunilem1  16158  psgnunilem2  16160  oddvds  16211  gexdvds  16244  sylow1lem1  16258  odcau  16264  pgpssslw  16274  sylow2alem2  16278  sylow2blem3  16282  fislw  16285  sylow2  16286  lsmmod  16333  efgredlem  16405  frgpup3  16436  gexex  16496  gsumval3OLD  16543  gsumval3  16546  gsumzres  16549  gsumzcl2  16550  gsumzf1o  16552  gsumzresOLD  16553  gsumzclOLD  16554  gsumzf1oOLD  16555  gsumzaddlem  16569  gsumzaddlemOLD  16571  gsumconst  16589  gsumzmhm  16592  gsumzmhmOLD  16593  gsumzoppg  16602  gsumzoppgOLD  16603  gsum2d2lem  16634  ablfac1eulem  16748  pgpfac1lem5  16755  ablfaclem3  16763  issubdrg  17066  lss1d  17220  lmhmeql  17312  lspextmo  17313  lspsnat  17402  lsppratlem6  17409  islbs3  17412  lbsextlem4  17418  lidl1el  17476  mvrf1  17675  mplsubglem  17687  mpllsslem  17688  mplsubglemOLD  17689  mpllsslemOLD  17690  mplcoe1  17721  mplcoe5  17725  mplcoe2OLD  17727  gsummoncoe1  17940  cnsubrg  18066  gsumfsum  18072  prmirredlem  18110  prmirredlemOLD  18113  znidomb  18187  frgpcyg  18199  cssmre  18311  dsmmsubg  18361  dsmmlss  18362  frlmsslsp  18416  frlmsslspOLD  18417  lindff1  18442  lindfrn  18443  mat1dimcrng  18566  mdetdiaglem  18672  mdetunilem7  18692  mdetunilem8  18693  mdetunilem9  18694  cpmatacl  18789  cpmatmcllem  18791  mp2pm2mplem4  18881  en2top  18989  toponmre  19096  topssnei  19127  innei  19128  clslp  19151  restcls  19184  restntr  19185  ordtrest2lem  19206  cnpco  19270  cncls2  19276  cncnpi  19281  cncnp  19283  cnconst2  19286  cnpdis  19296  lmcnp  19307  cnhaus  19357  nrmsep  19360  regsep2  19379  isreg2  19380  cncmp  19394  tgcmp  19403  sscmp  19407  cmpfi  19410  cnconn  19425  iunconlem  19430  clscon  19433  1stcfb  19448  1stcrest  19456  2ndcctbss  19458  2ndcdisj  19459  1stcelcls  19464  1stccnp  19465  restnlly  19485  cldllycmp  19498  lly1stc  19499  dislly  19500  kgentopon  19510  kgenidm  19519  1stckgenlem  19525  kgencn3  19530  ptpjpre1  19543  ptbasin  19549  txcls  19576  tx2cn  19582  ptpjcn  19583  ptclsg  19587  ptcnp  19594  txdis  19604  txlly  19608  txnlly  19609  pthaus  19610  txtube  19612  txcmplem1  19613  txcmplem2  19614  txcmp  19615  txhaus  19619  txkgen  19624  xkohaus  19625  xkococnlem  19631  xkococn  19632  txcon  19661  qtopeu  19688  qtoprest  19689  regr1lem2  19712  kqreglem1  19713  cmphaushmeo  19772  xkocnv  19786  fgabs  19851  filuni  19857  trufil  19882  ufileu  19891  filufint  19892  fin1aufil  19904  elfm2  19920  rnelfmlem  19924  fmfnfmlem2  19927  fmfnfmlem4  19929  fmufil  19931  flimopn  19947  fbflim2  19949  hausflimi  19952  hausflim  19953  flimcf  19954  flimclslem  19956  flimsncls  19958  hauspwpwf1  19959  cnpflfi  19971  fclsnei  19991  fclscf  19997  flimfnfcls  20000  fclscmp  20002  ufilcmp  20004  fcfnei  20007  cnpfcf  20013  alexsublem  20015  alexsub  20016  alexsubALTlem2  20019  alexsubALTlem3  20020  alexsubALTlem4  20021  ptcmplem3  20025  ptcmplem4  20026  ptcmplem5  20027  symgtgp  20071  tgpconcompeqg  20081  tgpconcomp  20082  ghmcnp  20084  tgpt0  20088  divstgplem  20090  haustsms2  20106  tsmsgsum  20108  tsmsgsumOLD  20111  tsmsresOLD  20116  tsmsres  20117  tsmsxp  20128  imasdsf1olem  20347  xbln0  20388  blssps  20398  blss  20399  neibl  20475  blcld  20479  metss  20482  metequiv2  20484  met1stc  20495  metrest  20498  prdsxmslem2  20503  metcnp3  20514  nrmmetd  20566  nlmvscnlem1  20666  nrginvrcnlem  20670  nmoleub  20709  icccmplem2  20799  icccmp  20801  reconnlem2  20803  xrge0tsms  20810  metdstri  20826  metdseq0  20829  metdscn  20831  cnmpt2pc  20899  cnheibor  20926  lebnumlem3  20934  pcoval2  20987  pcopt  20993  nmoleub2lem  21068  nmhmcn  21074  ipcnlem1  21156  cfilfcls  21184  cmetcaulem  21198  iscmet3lem2  21202  iscmet3  21203  equivcau  21210  caubl  21217  lmcau  21222  bcthlem2  21235  bcthlem3  21236  bcthlem4  21237  bcthlem5  21238  ivthlem2  21335  ivthlem3  21336  ovoliunlem2  21385  ovolicc2lem2  21400  ovolicc2lem3  21401  ovolicc2lem5  21403  ovolicc2  21404  ismbl2  21409  nulmbl  21417  nulmbl2  21418  unmbl  21419  shftmbl  21420  voliunlem3  21433  volsup  21437  ioombl1lem4  21442  ioombl1  21443  icombl  21445  ioombl  21446  uniioombl  21469  opnmbllem  21481  volivth  21487  vitali  21493  ismbf3d  21532  mbflimsup  21544  i1fadd  21573  itg1addlem4  21577  itg2le  21617  itg2seq  21620  itg2lea  21622  itg2splitlem  21626  itg2split  21627  itg2mono  21631  itg2gt0  21638  itg2cnlem2  21640  itgss  21689  itgfsum  21704  itgcn  21720  ellimc3  21754  limcco  21768  limciun  21769  dvnres  21805  dvnfre  21826  rolle  21862  c1liplem1  21868  dvivth  21882  dvne0  21883  lhop1lem  21885  lhop1  21886  lhop  21888  dvcnvrelem1  21889  dvfsumrlim  21903  dvfsum2  21906  ftc1a  21909  ftc1lem6  21913  itgsubst  21921  tdeglem4  21929  mdegaddle  21945  mdegvscale  21946  mdegmullem  21949  deg1tmle  21989  ply1divex  22008  dvdsq1p  22032  fta1g  22039  fta1b  22041  plyco0  22060  coeeulem  22092  dgrlem  22097  plyco  22109  coemullem  22117  dgreq0  22132  dgrco  22142  plydivex  22163  quotcan  22175  aannenlem1  22194  aalioulem2  22199  aalioulem3  22200  taylthlem1  22238  ulmbdd  22263  ulmdvlem3  22267  itgulm  22273  radcnvlt1  22283  psercnlem1  22290  abelthlem2  22297  abelthlem8  22304  logcnlem5  22491  efopn  22503  cxpmul2z  22536  cxpcn3lem  22585  cxpeq  22595  xrlimcnp  22762  cxplim  22765  o1cxp  22768  cxploglim  22771  scvxcvx  22779  jensen  22782  ftalem1  22810  ftalem2  22811  fta  22817  basellem3  22820  isppw2  22853  ppinprm  22890  chtnprm  22892  dvdsmulf1o  22934  chtublem  22950  perfectlem2  22969  dchrfi  22994  dchrptlem1  23003  dchrptlem2  23004  dchrptlem3  23005  dchrsum2  23007  bposlem1  23023  bposlem3  23025  2sqlem5  23107  2sqlem6  23108  2sqlem8  23111  2sqlem10  23113  2sqb  23117  chebbnd1lem1  23118  chtppilimlem2  23123  dchrisum0flb  23159  dchrisum0fno1  23160  dchrisum0  23169  pntrsumbnd2  23216  pntpbnd1  23235  pntpbnd2  23236  pntlemp  23259  pnt3  23261  qabvle  23274  ostth2lem2  23283  ostth3  23287  ostth  23288  colinearalglem4  23624  axcontlem10  23688  umgraex  23726  eupai  24057  isgrp2d  24191  ghgrp  24324  ghablo  24325  smcnlem  24561  ubthlem1  24740  ubthlem3  24742  htthlem  24788  pjhthlem2  25264  5oalem6  25531  leopmuli  26006  pjnormssi  26041  pjclem4  26072  pj3si  26080  hatomistici  26235  sumdmdlem  26291  suppss2f  26422  xrge0tsmsd  26710  isarchiofld  26742  ordtrest2NEWlem  26809  qqhf  26872  eulerpartlemb  27207  ballotlemfc0  27331  ballotlemfcc  27332  sgn3da  27380  subfacp1lem5  27528  erdszelem7  27541  erdszelem11  27545  pconcon  27576  txpcon  27577  conpcon  27580  sconpi1  27584  txscon  27586  cvxscon  27588  cvmopnlem  27623  cvmfolem  27624  cvmliftmolem2  27627  cvmliftlem7  27636  cvmliftlem10  27639  cvmliftlem15  27643  cvmlift2lem10  27657  cvmlift3lem4  27667  cvmlift3lem8  27671  prodmolem2  27904  zprod  27906  fprod  27910  fprodf1o  27915  prodss  27916  fprodss  27917  fprodcl2lem  27919  fprodmul  27927  fproddiv  27928  fprodconst  27945  fprodn0  27946  fprodcom2  27951  wzel  28217  wsuclem  28218  nofulllem4  28302  btwnouttr2  28509  cgrxfr  28542  btwnxfr  28543  brcolinear  28546  lineext  28563  btwnconn1lem13  28586  midofsegid  28591  segcon2  28592  brsegle  28595  seglecgr12im  28597  segletr  28601  colinbtwnle  28605  broutsideof2  28609  btwnoutside  28612  broutsideof3  28613  outsideoftr  28616  outsideofeq  28617  outsideofeu  28618  outsidele  28619  lineunray  28634  lineelsb2  28635  linethru  28640  wl-sbcom2d-lem1  28845  finixpnum  28874  supaddc  28877  heicant  28886  opnmbllem0  28887  mblfinlem3  28890  ismblfin  28892  ovoliunnfl  28893  voliunnfl  28895  volsupnfl  28896  itg2addnclem  28903  itg2addnclem3  28905  ftc1cnnc  28926  finminlem  28973  nn0prpwlem  28977  locfincmp  29036  comppfsc  29039  neibastop2lem  29041  neibastop2  29042  neibastop3  29043  topjoin  29046  tailfb  29058  sdclem2  29098  fdc  29101  istotbnd3  29130  isbnd2  29142  isbnd3  29143  prdsbnd  29152  cntotbnd  29155  heibor1lem  29168  heibor1  29169  heiborlem10  29179  rrncmslem  29191  ghomco  29208  1idl  29286  unichnidl  29291  prtlem10  29470  prtlem18  29482  isnacs3  29506  nacsfix  29508  fnwe2lem2  29864  kelac1  29876  unxpwdom3  29908  hbtlem5  29944  hbt  29946  dgraa0p  29966  hashgcdeq  30026  rlimdmafv  30960  numclwwlkovf2ex  31556  lindslinindsimp2  31769  atlatmstc  33815  cvrexchlem  33914  paddasslem14  34328  pexmidlem5N  34469  cdleme29ex  34869  cdlemefr29exN  34897  cdleme32fva  34932  diarnN  35625  dihlsscpre  35730
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