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

Theorem expr 602
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 592 . 2
32imp 422 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362
This theorem is referenced by:  reximddv  2808  rexlimdvaa  2821  disjxiun  4264  wereu2  4688  suppssOLD  5806  fcof1  5959  knatar  6016  riota5f  6046  ovmpt2df  6192  suppss2OLD  6285  extmptsuppeq  6679  suppss  6684  suppss2  6688  smoord  6785  tfrlem9a  6804  oaass  6961  oelimcl  7000  oaabs2  7045  swoso  7093  eceqoveq  7166  domdifsn  7353  domunsncan  7370  omxpenlem  7371  enfixsn  7379  mapdom2  7441  frfi  7516  fofinf1o  7551  finsschain  7577  elfiun  7627  marypha1lem  7630  eqsupd  7654  ordiso2  7676  ordtypelem6  7684  ordtypelem7  7685  ordtypelem10  7688  oismo  7701  wemapsolem  7711  brwdom2  7735  wdomtr  7737  unwdomg  7746  xpwdomg  7747  unxpwdom2  7750  cantnfval2  7824  cantnfle  7826  cantnflem1  7844  cantnf  7848  cantnfval2OLD  7854  cantnfleOLD  7856  cantnflem1OLD  7867  cantnfOLD  7870  r1ordg  7932  tcrank  8038  carddomi2  8087  harval2  8114  infxpenlem  8127  infxpenc2lem2  8133  infxpenc2lem2OLD  8137  fseqenlem1  8141  dfac8clem  8149  acndom2  8171  infpwfien  8179  iunfictbso  8231  dfac12lem3  8261  infxp  8331  coflim  8377  cofsmo  8385  coftr  8389  sornom  8393  infpssrlem4  8422  enfin2i  8437  fin23lem26  8441  fin23lem27  8444  fin23lem36  8464  fin23lem40  8467  isf32lem5  8473  isf34lem4  8493  isfin1-3  8502  fin1a2lem10  8525  fin1a2lem13  8528  fin1a2s  8530  hsmexlem4  8545  ttukeylem5  8629  ttukeylem6  8630  ttukeylem7  8631  alephval2  8683  gchor  8740  fpwwe2lem7  8749  fpwwe2lem12  8754  fpwwe2  8756  pwfseqlem4a  8774  pwfseqlem4  8775  winalim2  8809  gchina  8812  inar1  8888  nqereq  9050  prlem934  9148  prlem936  9162  supsrlem  9224  axpre-sup  9282  dedekind  9479  dedekindle  9480  prodge0  10122  mulge0b  10145  supmul1  10241  un0addcl  10559  un0mulcl  10560  uzwo3  10893  qbtwnre  11114  xlemul1a  11196  seqcl2  11765  seqfveq2  11769  seqshft2  11773  monoord  11777  seqsplit  11780  seqf1olem1  11786  seqid2  11793  seqhomo  11794  expnegz  11839  expcan  11857  ltexp2  11858  discr  11942  bcval5  12035  hashbc  12147  hashf1lem2  12150  seqcoll  12157  seqcoll2  12158  wrdind  12312  wrd2ind  12313  cau3lem  12783  ello1d  12942  lo1bdd2  12943  rlimclim  12965  climrlim2  12966  rlimdm  12970  rlimcn1  13007  reccn2  13015  rlimsqzlem  13067  lo1le  13070  caucvgrlem  13091  caurcvg2  13096  summolem2  13134  zsum  13136  fsum  13138  fsumf1o  13141  sumss  13142  fsumss  13143  fsumcl2lem  13149  fsumadd  13156  fsumcom2  13182  fsum0diag2  13190  fsummulc2  13191  fsumconst  13197  fsumrelem  13210  fsumrlim  13214  fsumo1  13215  divrcnv  13255  geomulcvg  13276  mertenslem2  13285  ruclem8  13459  dvds0lem  13483  dvdsnegb  13490  dvdssub2  13510  bitsf1  13582  bitsshft  13611  bezoutlem3  13664  bezoutlem4  13665  isprm2lem  13710  isprm6  13735  isprm5  13738  modprminv  13810  modprminveq  13811  reumodprminv  13812  pcqmul  13860  pcqcl  13863  pcxcl  13867  pc2dvds  13885  pcadd  13891  pcmpt  13894  pockthg  13907  infpnlem1  13911  prmreclem5  13921  vdwlem2  13983  vdwlem9  13990  vdwlem10  13991  vdwlem12  13993  ramub  14014  0ram  14021  ramub1lem2  14028  ramub1  14029  ramcl  14030  mreexexd  14526  acsfn2  14541  iscatd  14551  catpropd  14588  setcmon  14895  drsdirfi  15048  pleval2i  15074  psss  15324  mhmeql  15431  gsumvallem1  15439  frmdss2  15478  frmdup3  15481  grprcan  15508  mulgnn0ass  15593  isnsg3  15652  ghmpreima  15705  ghmeql  15706  gaorber  15763  f1omvdco2  15891  psgnunilem1  15936  psgnunilem2  15938  oddvds  15987  gexdvds  16020  sylow1lem1  16034  odcau  16040  pgpssslw  16050  sylow2alem2  16054  sylow2blem3  16058  fislw  16061  sylow2  16062  lsmmod  16109  efgredlem  16181  frgpup3  16212  gexex  16271  gsumval3  16317  gsumzres  16320  gsumzcl  16321  gsumzf1o  16322  gsumzaddlem  16329  gsumconst  16336  gsumzmhm  16337  gsumzoppg  16343  gsum2d2lem  16356  ablfac1eulem  16439  pgpfac1lem5  16446  ablfaclem3  16454  issubdrg  16703  lss1d  16853  lmhmeql  16945  lspextmo  16946  lspsnat  17035  lsppratlem6  17042  islbs3  17045  lbsextlem4  17051  lidl1el  17109  mvrf1  17309  mplsubglem  17321  mpllsslem  17322  mplcoe1  17351  mplcoe2  17353  cnsubrg  17583  gsumfsum  17589  prmirredlem  17625  prmirredlemOLD  17628  znidomb  17702  frgpcyg  17714  cssmre  17826  dsmmsubg  17876  dsmmlss  17877  frlmsslsp  17924  lindff1  17948  lindfrn  17949  mdet1  18110  mdetunilem7  18126  mdetunilem8  18127  mdetunilem9  18128  en2top  18294  toponmre  18401  topssnei  18432  innei  18433  clslp  18456  restcls  18489  restntr  18490  ordtrest2lem  18511  cnpco  18575  cncls2  18581  cncnpi  18586  cncnp  18588  cnconst2  18591  cnpdis  18601  lmcnp  18612  cnhaus  18662  nrmsep  18665  regsep2  18684  isreg2  18685  cncmp  18699  tgcmp  18708  sscmp  18712  cmpfi  18715  cnconn  18730  iunconlem  18735  clscon  18738  1stcfb  18753  1stcrest  18761  2ndcctbss  18763  2ndcdisj  18764  1stcelcls  18769  1stccnp  18770  restnlly  18790  cldllycmp  18803  lly1stc  18804  dislly  18805  kgentopon  18815  kgenidm  18824  1stckgenlem  18830  kgencn3  18835  ptpjpre1  18848  ptbasin  18854  txcls  18881  tx2cn  18887  ptpjcn  18888  ptclsg  18892  ptcnp  18899  txdis  18909  txlly  18913  txnlly  18914  pthaus  18915  txtube  18917  txcmplem1  18918  txcmplem2  18919  txcmp  18920  txhaus  18924  txkgen  18929  xkohaus  18930  xkococnlem  18936  xkococn  18937  txcon  18966  qtopeu  18993  qtoprest  18994  regr1lem2  19017  kqreglem1  19018  cmphaushmeo  19077  xkocnv  19091  fgabs  19156  filuni  19162  trufil  19187  ufileu  19196  filufint  19197  fin1aufil  19209  elfm2  19225  rnelfmlem  19229  fmfnfmlem2  19232  fmfnfmlem4  19234  fmufil  19236  flimopn  19252  fbflim2  19254  hausflimi  19257  hausflim  19258  flimcf  19259  flimclslem  19261  flimsncls  19263  hauspwpwf1  19264  cnpflfi  19276  fclsnei  19296  fclscf  19302  flimfnfcls  19305  fclscmp  19307  ufilcmp  19309  fcfnei  19312  cnpfcf  19318  alexsublem  19320  alexsub  19321  alexsubALTlem2  19324  alexsubALTlem3  19325  alexsubALTlem4  19326  ptcmplem3  19330  ptcmplem4  19331  ptcmplem5  19332  symgtgp  19376  tgpconcompeqg  19386  tgpconcomp  19387  ghmcnp  19389  tgpt0  19393  divstgplem  19395  haustsms2  19411  tsmsgsum  19413  tsmsres  19418  tsmsxp  19429  imasdsf1olem  19648  xbln0  19689  blssps  19699  blss  19700  neibl  19776  blcld  19780  metss  19783  metequiv2  19785  met1stc  19796  metrest  19799  prdsxmslem2  19804  metcnp3  19815  nrmmetd  19867  nlmvscnlem1  19967  nrginvrcnlem  19971  nmoleub  20010  icccmplem2  20100  icccmp  20102  reconnlem2  20104  xrge0tsms  20111  metdstri  20127  metdseq0  20130  metdscn  20132  cnmpt2pc  20200  cnheibor  20227  lebnumlem3  20235  pcoval2  20288  pcopt  20294  nmoleub2lem  20369  nmhmcn  20375  ipcnlem1  20457  cfilfcls  20485  cmetcaulem  20499  iscmet3lem2  20503  iscmet3  20504  equivcau  20511  caubl  20518  lmcau  20523  bcthlem2  20536  bcthlem3  20537  bcthlem4  20538  bcthlem5  20539  ivthlem2  20636  ivthlem3  20637  ovoliunlem2  20686  ovolicc2lem2  20701  ovolicc2lem3  20702  ovolicc2lem5  20704  ovolicc2  20705  ismbl2  20710  nulmbl  20717  nulmbl2  20718  unmbl  20719  shftmbl  20720  voliunlem3  20733  volsup  20737  ioombl1lem4  20742  ioombl1  20743  icombl  20745  ioombl  20746  uniioombl  20769  opnmbllem  20781  volivth  20787  vitali  20793  ismbf3d  20832  mbflimsup  20844  i1fadd  20873  itg1addlem4  20877  itg2le  20917  itg2seq  20920  itg2lea  20922  itg2splitlem  20926  itg2split  20927  itg2mono  20931  itg2gt0  20938  itg2cnlem2  20940  itgss  20989  itgfsum  21004  itgcn  21020  ellimc3  21054  limcco  21068  limciun  21069  dvnres  21105  dvnfre  21126  rolle  21162  c1liplem1  21168  dvivth  21182  dvne0  21183  lhop1lem  21185  lhop1  21186  lhop  21188  dvcnvrelem1  21189  dvfsumrlim  21203  dvfsum2  21206  ftc1a  21209  ftc1lem6  21213  itgsubst  21221  tdeglem4  21271  mdegaddle  21287  mdegvscale  21288  mdegmullem  21291  deg1tmle  21330  ply1divex  21349  dvdsq1p  21373  fta1g  21380  fta1b  21382  plyco0  21401  coeeulem  21433  dgrlem  21438  plyco  21450  coemullem  21458  dgreq0  21473  dgrco  21483  plydivex  21504  quotcan  21516  aannenlem1  21535  aalioulem2  21540  aalioulem3  21541  taylthlem1  21579  ulmbdd  21604  ulmdvlem3  21608  itgulm  21614  radcnvlt1  21624  psercnlem1  21631  abelthlem2  21638  abelthlem8  21645  logcnlem5  21832  efopn  21844  cxpmul2z  21877  cxpcn3lem  21926  cxpeq  21936  xrlimcnp  22103  cxplim  22106  o1cxp  22109  cxploglim  22112  scvxcvx  22120  jensen  22123  ftalem1  22151  ftalem2  22152  fta  22158  basellem3  22161  isppw2  22194  ppinprm  22231  chtnprm  22233  dvdsmulf1o  22275  chtublem  22291  perfectlem2  22310  dchrfi  22335  dchrptlem1  22344  dchrptlem2  22345  dchrptlem3  22346  dchrsum2  22348  bposlem1  22364  bposlem3  22366  2sqlem5  22448  2sqlem6  22449  2sqlem8  22452  2sqlem10  22454  2sqb  22458  chebbnd1lem1  22459  chtppilimlem2  22464  dchrisum0flb  22500  dchrisum0fno1  22501  dchrisum0  22510  pntrsumbnd2  22557  pntpbnd1  22576  pntpbnd2  22577  pntlemp  22600  pnt3  22602  qabvle  22615  ostth2lem2  22624  ostth3  22628  ostth  22629  colinearalglem4  22834  axcontlem10  22898  umgraex  22936  eupai  23267  isgrp2d  23401  ghgrp  23534  ghablo  23535  smcnlem  23771  ubthlem1  23950  ubthlem3  23952  htthlem  23998  pjhthlem2  24474  5oalem6  24741  leopmuli  25216  pjnormssi  25251  pjclem4  25282  pj3si  25290  hatomistici  25445  sumdmdlem  25501  suppss2f  25634  xrge0tsmsd  25961  isarchiofld  25993  ordtrest2NEWlem  26061  qqhf  26124  eulerpartlemb  26454  ballotlemfc0  26578  ballotlemfcc  26579  sgn3da  26627  subfacp1lem5  26775  erdszelem7  26788  erdszelem11  26792  pconcon  26823  txpcon  26824  conpcon  26827  sconpi1  26831  txscon  26833  cvxscon  26835  cvmopnlem  26870  cvmfolem  26871  cvmliftmolem2  26874  cvmliftlem7  26883  cvmliftlem10  26886  cvmliftlem15  26890  cvmlift2lem10  26904  cvmlift3lem4  26914  cvmlift3lem8  26918  prodmolem2  27150  zprod  27152  fprod  27156  fprodf1o  27161  prodss  27162  fprodss  27163  fprodcl2lem  27165  fprodmul  27173  fproddiv  27174  fprodconst  27191  fprodn0  27192  fprodcom2  27197  wzel  27463  wsuclem  27464  nofulllem4  27548  btwnouttr2  27755  cgrxfr  27788  btwnxfr  27789  brcolinear  27792  lineext  27809  btwnconn1lem13  27832  midofsegid  27837  segcon2  27838  brsegle  27841  seglecgr12im  27843  segletr  27847  colinbtwnle  27851  broutsideof2  27855  btwnoutside  27858  broutsideof3  27859  outsideoftr  27862  outsideofeq  27863  outsideofeu  27864  outsidele  27865  lineunray  27880  lineelsb2  27881  linethru  27886  finixpnum  28085  supaddc  28088  heicant  28097  opnmbllem0  28098  mblfinlem3  28101  ismblfin  28103  ovoliunnfl  28104  voliunnfl  28106  volsupnfl  28107  itg2addnclem  28114  itg2addnclem3  28116  ftc1cnnc  28137  finminlem  28184  nn0prpwlem  28188  locfincmp  28247  comppfsc  28250  neibastop2lem  28252  neibastop2  28253  neibastop3  28254  topjoin  28257  tailfb  28269  sdclem2  28309  fdc  28312  istotbnd3  28341  isbnd2  28353  isbnd3  28354  prdsbnd  28363  cntotbnd  28366  heibor1lem  28379  heibor1  28380  heiborlem10  28390  rrncmslem  28402  ghomco  28419  1idl  28497  unichnidl  28502  prtlem10  28682  prtlem18  28694  isnacs3  28718  nacsfix  28720  fnwe2lem2  29077  kelac1  29089  unxpwdom3  29121  hbtlem5  29157  hbt  29159  dgraa0p  29179  hashgcdeq  29239  rlimdmafv  29757  numclwwlkovf2ex  30353  gsumXval3  30465  gsumXzres  30467  gsumXzcl2  30468  gsumXzf1o  30470  gsumXzaddlem  30478  gsumXconst  30484  gsumXzmhm  30485  gsumXzoppg  30491  gsumX2d2lem  30505  frlmXsslsp  30520  lindslinindsimp2  30581  atlatmstc  32401  cvrexchlem  32500  paddasslem14  32914  pexmidlem5N  33055  cdleme29ex  33455  cdlemefr29exN  33483  cdleme32fva  33518  diarnN  34211  dihlsscpre  34316
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 179  df-an 364
  Copyright terms: Public domain W3C validator