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

Theorem expr 600
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 590 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 420 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  rexlimdvaa  2837  disjxiun  4234  wereu2  4608  suppss  5892  fcof1  6049  knatar  6109  ovmpt2df  6234  suppss2  6329  riota5f  6603  smoord  6656  tfrlem9a  6676  oaass  6833  oelimcl  6872  oaabs2  6917  swoso  6965  eceqoveq  7038  domdifsn  7220  domunsncan  7237  omxpenlem  7238  mapdom2  7307  frfi  7381  fofinf1o  7416  finsschain  7442  elfiun  7464  marypha1lem  7467  eqsupd  7491  ordiso2  7513  ordtypelem6  7521  ordtypelem7  7522  ordtypelem10  7525  oismo  7538  wemapso2lem  7548  brwdom2  7570  wdomtr  7572  unwdomg  7581  xpwdomg  7582  unxpwdom2  7585  cantnfval2  7653  cantnfle  7655  cantnfreslem  7660  cantnflem1  7674  cantnf  7678  r1ordg  7733  tcrank  7839  carddomi2  7888  harval2  7915  infxpenlem  7926  infxpenc2lem2  7932  fseqenlem1  7936  dfac8clem  7944  acndom2  7966  infpwfien  7974  iunfictbso  8026  dfac12lem3  8056  infxp  8126  coflim  8172  cofsmo  8180  coftr  8184  sornom  8188  infpssrlem4  8217  enfin2i  8232  fin23lem26  8236  fin23lem27  8239  fin23lem36  8259  fin23lem40  8262  isf32lem5  8268  isf34lem4  8288  isfin1-3  8297  fin1a2lem10  8320  fin1a2lem13  8323  fin1a2s  8325  hsmexlem4  8340  ttukeylem5  8424  ttukeylem6  8425  ttukeylem7  8426  alephval2  8478  gchor  8533  fpwwe2lem7  8542  fpwwe2lem12  8547  fpwwe2  8549  pwfseqlem4a  8567  pwfseqlem4  8568  winalim2  8602  gchina  8605  inar1  8681  nqereq  8843  prlem934  8941  prlem936  8955  supsrlem  9017  axpre-sup  9075  prodge0  9888  supmul1  10004  un0addcl  10284  un0mulcl  10285  uzwo3  10600  qbtwnre  10816  xlemul1a  10898  seqcl2  11372  seqfveq2  11376  seqshft2  11380  monoord  11384  seqsplit  11387  seqf1olem1  11393  seqid2  11400  seqhomo  11401  expnegz  11445  expcan  11463  ltexp2  11464  discr  11547  bcval5  11640  hashbc  11733  hashf1lem2  11736  seqcoll  11743  seqcoll2  11744  wrdind  11822  cau3lem  12189  ello1d  12348  lo1bdd2  12349  rlimclim  12371  climrlim2  12372  rlimdm  12376  rlimcn1  12413  reccn2  12421  rlimsqzlem  12473  lo1le  12476  caucvgrlem  12497  caurcvg2  12502  summolem2  12541  zsum  12543  fsum  12545  fsumf1o  12548  sumss  12549  fsumss  12550  fsumcl2lem  12556  fsumadd  12563  fsumcom2  12589  fsum0diag2  12597  fsummulc2  12598  fsumconst  12604  fsumrelem  12617  fsumrlim  12621  fsumo1  12622  divrcnv  12663  geomulcvg  12684  mertenslem2  12693  ruclem8  12867  dvds0lem  12891  dvdsnegb  12898  dvdssub2  12918  bitsf1  12989  bitsshft  13018  bezoutlem3  13071  bezoutlem4  13072  isprm2lem  13117  isprm6  13140  isprm5  13143  pcqmul  13258  pcqcl  13261  pcxcl  13265  pc2dvds  13283  pcadd  13289  pcmpt  13292  pockthg  13305  infpnlem1  13309  prmreclem5  13319  vdwlem2  13381  vdwlem9  13388  vdwlem10  13389  vdwlem12  13391  ramub  13412  0ram  13419  ramub1lem2  13426  ramub1  13427  ramcl  13428  mreexexd  13904  acsfn2  13919  iscatd  13929  catpropd  13966  setcmon  14273  drsdirfi  14426  pleval2i  14452  psss  14677  mhmeql  14795  gsumvallem1  14802  frmdss2  14839  frmdup3  14842  grprcan  14869  mulgnn0ass  14950  isnsg3  15005  ghmpreima  15058  ghmeql  15059  gaorber  15116  oddvds  15216  gexdvds  15249  sylow1lem1  15263  odcau  15269  pgpssslw  15279  sylow2alem2  15283  sylow2blem3  15287  fislw  15290  sylow2  15291  lsmmod  15338  efgredlem  15410  frgpup3  15441  gexex  15499  gsumval3  15545  gsumzres  15548  gsumzcl  15549  gsumzf1o  15550  gsumzaddlem  15557  gsumconst  15563  gsumzmhm  15564  gsumzoppg  15570  gsum2d2lem  15578  ablfac1eulem  15661  pgpfac1lem5  15668  ablfaclem3  15676  issubdrg  15924  lss1d  16070  lmhmeql  16162  lspextmo  16163  lspsnat  16248  lsppratlem6  16255  islbs3  16258  lbsextlem4  16264  lidl1el  16320  mvrf1  16520  mplsubglem  16529  mpllsslem  16530  mplcoe1  16559  mplcoe2  16561  cnsubrg  16790  gsumfsum  16797  prmirredlem  16804  znidomb  16873  frgpcyg  16885  cssmre  16951  en2top  17081  toponmre  17188  topssnei  17219  innei  17220  clslp  17243  restcls  17276  restntr  17277  ordtrest2lem  17298  cnpco  17362  cncls2  17368  cncnpi  17373  cncnp  17375  cnconst2  17378  cnpdis  17388  lmcnp  17399  cnhaus  17449  nrmsep  17452  regsep2  17471  isreg2  17472  cncmp  17486  tgcmp  17495  sscmp  17499  cmpfi  17502  cnconn  17516  iunconlem  17521  clscon  17524  1stcfb  17539  1stcrest  17547  2ndcctbss  17549  2ndcdisj  17550  1stcelcls  17555  1stccnp  17556  restnlly  17576  cldllycmp  17589  lly1stc  17590  dislly  17591  kgentopon  17601  kgenidm  17610  1stckgenlem  17616  kgencn3  17621  ptpjpre1  17634  ptbasin  17640  txcls  17667  tx2cn  17673  ptpjcn  17674  ptclsg  17678  ptcnp  17685  txdis  17695  txlly  17699  txnlly  17700  pthaus  17701  txtube  17703  txcmplem1  17704  txcmplem2  17705  txcmp  17706  txhaus  17710  txkgen  17715  xkohaus  17716  xkococnlem  17722  xkococn  17723  txcon  17752  qtopeu  17779  qtoprest  17780  regr1lem2  17803  kqreglem1  17804  cmphaushmeo  17863  xkocnv  17877  fgabs  17942  filuni  17948  trufil  17973  ufileu  17982  filufint  17983  fin1aufil  17995  elfm2  18011  rnelfmlem  18015  fmfnfmlem2  18018  fmfnfmlem4  18020  fmufil  18022  flimopn  18038  fbflim2  18040  hausflimi  18043  hausflim  18044  flimcf  18045  flimclslem  18047  flimsncls  18049  hauspwpwf1  18050  cnpflfi  18062  fclsnei  18082  fclscf  18088  flimfnfcls  18091  fclscmp  18093  ufilcmp  18095  fcfnei  18098  cnpfcf  18104  alexsublem  18106  alexsub  18107  alexsubALTlem2  18110  alexsubALTlem3  18111  alexsubALTlem4  18112  ptcmplem3  18116  ptcmplem4  18117  ptcmplem5  18118  symgtgp  18162  tgpconcompeqg  18172  tgpconcomp  18173  ghmcnp  18175  tgpt0  18179  divstgplem  18181  haustsms2  18197  tsmsgsum  18199  tsmsres  18204  tsmsxp  18215  imasdsf1olem  18434  xbln0  18475  blssps  18485  blss  18486  neibl  18562  blcld  18566  metss  18569  metequiv2  18571  met1stc  18582  metrest  18585  prdsxmslem2  18590  metcnp3  18601  nrmmetd  18653  nlmvscnlem1  18753  nrginvrcnlem  18757  nmoleub  18796  icccmplem2  18885  icccmp  18887  reconnlem2  18889  xrge0tsms  18896  metdstri  18912  metdseq0  18915  metdscn  18917  cnmpt2pc  18984  cnheibor  19011  lebnumlem3  19019  pcoval2  19072  pcopt  19078  nmoleub2lem  19153  nmhmcn  19159  ipcnlem1  19230  cfilfcls  19258  cmetcaulem  19272  iscmet3lem2  19276  iscmet3  19277  equivcau  19284  caubl  19291  lmcau  19296  bcthlem2  19309  bcthlem3  19310  bcthlem4  19311  bcthlem5  19312  ivthlem2  19380  ivthlem3  19381  ovoliunlem2  19430  ovolicc2lem2  19445  ovolicc2lem3  19446  ovolicc2lem5  19448  ovolicc2  19449  ismbl2  19454  nulmbl  19461  nulmbl2  19462  unmbl  19463  shftmbl  19464  voliunlem3  19477  volsup  19481  ioombl1lem4  19486  ioombl1  19487  icombl  19489  ioombl  19490  uniioombl  19512  opnmbllem  19524  volivth  19530  vitali  19536  ismbf3d  19575  mbflimsup  19587  i1fadd  19616  itg1addlem4  19620  itg2le  19660  itg2seq  19663  itg2lea  19665  itg2splitlem  19669  itg2split  19670  itg2mono  19674  itg2gt0  19681  itg2cnlem2  19683  itgss  19732  itgfsum  19747  itgcn  19763  ellimc3  19797  limcco  19811  limciun  19812  dvnres  19848  dvnfre  19869  rolle  19905  c1liplem1  19911  dvivth  19925  dvne0  19926  lhop1lem  19928  lhop1  19929  lhop  19931  dvcnvrelem1  19932  dvfsumrlim  19946  dvfsum2  19949  ftc1a  19952  ftc1lem6  19956  itgsubst  19964  tdeglem4  20014  mdegaddle  20028  mdegvscale  20029  mdegmullem  20032  deg1tmle  20071  ply1divex  20090  dvdsq1p  20114  fta1g  20121  fta1b  20123  plyco0  20142  coeeulem  20174  dgrlem  20179  plyco  20191  coemullem  20199  dgreq0  20214  dgrco  20224  plydivex  20245  quotcan  20257  aannenlem1  20276  aalioulem2  20281  aalioulem3  20282  taylthlem1  20320  ulmbdd  20345  ulmdvlem3  20349  itgulm  20355  radcnvlt1  20365  psercnlem1  20372  abelthlem2  20379  abelthlem8  20386  logcnlem5  20568  efopn  20580  cxpmul2z  20613  cxpcn3lem  20662  cxpeq  20672  xrlimcnp  20838  cxplim  20841  o1cxp  20844  cxploglim  20847  scvxcvx  20855  jensen  20858  ftalem1  20886  ftalem2  20887  fta  20893  basellem3  20896  isppw2  20929  ppinprm  20966  chtnprm  20968  dvdsmulf1o  21010  chtublem  21026  perfectlem2  21045  dchrfi  21070  dchrptlem1  21079  dchrptlem2  21080  dchrptlem3  21081  dchrsum2  21083  bposlem1  21099  bposlem3  21101  2sqlem5  21183  2sqlem6  21184  2sqlem8  21187  2sqlem10  21189  2sqb  21193  chebbnd1lem1  21194  chtppilimlem2  21199  dchrisum0flb  21235  dchrisum0fno1  21236  dchrisum0  21245  pntrsumbnd2  21292  pntpbnd1  21311  pntpbnd2  21312  pntlemp  21335  pnt3  21337  qabvle  21350  ostth2lem2  21359  ostth3  21363  ostth  21364  umgraex  21389  eupai  21720  isgrp2d  21854  ghgrp  21987  ghablo  21988  smcnlem  22224  ubthlem1  22403  ubthlem3  22405  htthlem  22451  pjhthlem2  22925  5oalem6  23192  leopmuli  23667  pjnormssi  23702  pjclem4  23733  pj3si  23741  hatomistici  23896  sumdmdlem  23952  reximddv  23993  suppss2f  24080  xrge0tsmsd  24254  qqhf  24401  ballotlemfc0  24781  ballotlemfcc  24782  subfacp1lem5  24901  erdszelem7  24914  erdszelem11  24918  pconcon  24949  txpcon  24950  conpcon  24953  sconpi1  24957  txscon  24959  cvxscon  24961  cvmopnlem  24996  cvmfolem  24997  cvmliftmolem2  25000  cvmliftlem7  25009  cvmliftlem10  25012  cvmliftlem15  25016  cvmlift2lem10  25030  cvmlift3lem4  25040  cvmlift3lem8  25044  dedekind  25218  dedekindle  25219  mulge0b  25222  prodmolem2  25292  zprod  25294  fprod  25298  fprodf1o  25303  prodss  25304  fprodss  25305  fprodcl2lem  25307  fprodmul  25315  fproddiv  25316  fprodconst  25333  fprodn0  25334  fprodcom2  25339  wzel  25606  wsuclem  25607  nofulllem4  25691  colinearalglem4  25879  axcontlem10  25943  btwnouttr2  25987  cgrxfr  26020  btwnxfr  26021  brcolinear  26024  lineext  26041  btwnconn1lem13  26064  midofsegid  26069  segcon2  26070  brsegle  26073  seglecgr12im  26075  segletr  26079  colinbtwnle  26083  broutsideof2  26087  btwnoutside  26090  broutsideof3  26091  outsideoftr  26094  outsideofeq  26095  outsideofeu  26096  outsidele  26097  lineunray  26112  lineelsb2  26113  linethru  26118  supaddc  26269  heicant  26277  opnmbllem0  26278  mblfinlem3  26281  ismblfin  26283  ovoliunnfl  26284  voliunnfl  26286  volsupnfl  26287  itg2addnclem  26294  itg2addnclem3  26296  ftc1cnnc  26317  finminlem  26359  nn0prpwlem  26363  locfincmp  26422  comppfsc  26425  neibastop2lem  26427  neibastop2  26428  neibastop3  26429  topjoin  26432  tailfb  26444  sdclem2  26484  fdc  26487  istotbnd3  26518  isbnd2  26530  isbnd3  26531  prdsbnd  26540  cntotbnd  26543  heibor1lem  26556  heibor1  26557  heiborlem10  26567  rrncmslem  26579  ghomco  26596  1idl  26674  unichnidl  26679  prtlem10  26752  prtlem18  26764  isnacs3  26802  nacsfix  26804  fnwe2lem2  27164  kelac1  27176  dsmmsubg  27224  dsmmlss  27225  frlmsslsp  27263  unxpwdom3  27271  enfixsn  27272  lindff1  27305  lindfrn  27306  hbtlem5  27347  hbt  27349  dgraa0p  27369  f1omvdco2  27406  psgnunilem1  27431  psgnunilem2  27433  hashgcdeq  27532  rlimdmafv  28055  modprminv  28283  modprminveq  28284  reumodprminv  28285  cshwidx  28300  atlatmstc  30215  cvrexchlem  30314  paddasslem14  30728  pexmidlem5N  30869  cdleme29ex  31269  cdlemefr29exN  31297  cdleme32fva  31332  diarnN  32025  dihlsscpre  32130
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 362
  Copyright terms: Public domain W3C validator