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

Theorem expr 599
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 589 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  rexlimdvaa  2774  disjxiun  4150  wereu2  4520  suppss  5802  fcof1  5959  knatar  6019  ovmpt2df  6144  suppss2  6239  riota5f  6510  smoord  6563  tfrlem9a  6583  oaass  6740  oelimcl  6779  oaabs2  6824  swoso  6872  eceqoveq  6945  domdifsn  7127  domunsncan  7144  omxpenlem  7145  mapdom2  7214  frfi  7288  fofinf1o  7323  finsschain  7348  elfiun  7370  marypha1lem  7373  eqsupd  7395  ordiso2  7417  ordtypelem6  7425  ordtypelem7  7426  ordtypelem10  7429  oismo  7442  wemapso2lem  7452  brwdom2  7474  wdomtr  7476  unwdomg  7485  xpwdomg  7486  unxpwdom2  7489  cantnfval2  7557  cantnfle  7559  cantnfreslem  7564  cantnflem1  7578  cantnf  7582  r1ordg  7637  tcrank  7741  carddomi2  7790  harval2  7817  infxpenlem  7828  infxpenc2lem2  7834  fseqenlem1  7838  dfac8clem  7846  acndom2  7868  infpwfien  7876  iunfictbso  7928  dfac12lem3  7958  infxp  8028  coflim  8074  cofsmo  8082  coftr  8086  sornom  8090  infpssrlem4  8119  enfin2i  8134  fin23lem26  8138  fin23lem27  8141  fin23lem36  8161  fin23lem40  8164  isf32lem5  8170  isf34lem4  8190  isfin1-3  8199  fin1a2lem10  8222  fin1a2lem13  8225  fin1a2s  8227  hsmexlem4  8242  ttukeylem5  8326  ttukeylem6  8327  ttukeylem7  8328  alephval2  8380  gchor  8435  fpwwe2lem7  8444  fpwwe2lem12  8449  fpwwe2  8451  pwfseqlem4a  8469  pwfseqlem4  8470  winalim2  8504  gchina  8507  inar1  8583  nqereq  8745  prlem934  8843  prlem936  8857  supsrlem  8919  axpre-sup  8977  prodge0  9789  supmul1  9905  un0addcl  10185  un0mulcl  10186  uzwo3  10501  qbtwnre  10717  xlemul1a  10799  seqcl2  11268  seqfveq2  11272  seqshft2  11276  monoord  11280  seqsplit  11283  seqf1olem1  11289  seqid2  11296  seqhomo  11297  expnegz  11341  expcan  11359  ltexp2  11360  discr  11443  bcval5  11536  hashbc  11629  hashf1lem2  11632  seqcoll  11639  seqcoll2  11640  wrdind  11718  cau3lem  12085  ello1d  12244  lo1bdd2  12245  rlimclim  12267  climrlim2  12268  rlimdm  12272  rlimcn1  12309  reccn2  12317  rlimsqzlem  12369  lo1le  12372  caucvgrlem  12393  caurcvg2  12398  summolem2  12437  zsum  12439  fsum  12441  fsumf1o  12444  sumss  12445  fsumss  12446  fsumcl2lem  12452  fsumadd  12459  fsumcom2  12485  fsum0diag2  12493  fsummulc2  12494  fsumconst  12500  fsumrelem  12513  fsumrlim  12517  fsumo1  12518  divrcnv  12559  geomulcvg  12580  mertenslem2  12589  ruclem8  12763  dvds0lem  12787  dvdsnegb  12794  dvdssub2  12814  bitsf1  12885  bitsshft  12914  bezoutlem3  12967  bezoutlem4  12968  isprm2lem  13013  isprm6  13036  isprm5  13039  pcqmul  13154  pcqcl  13157  pcxcl  13161  pc2dvds  13179  pcadd  13185  pcmpt  13188  pockthg  13201  infpnlem1  13205  prmreclem5  13215  vdwlem2  13277  vdwlem9  13284  vdwlem10  13285  vdwlem12  13287  ramub  13308  0ram  13315  ramub1lem2  13322  ramub1  13323  ramcl  13324  mreexexd  13800  acsfn2  13815  iscatd  13825  catpropd  13862  setcmon  14169  drsdirfi  14322  pleval2i  14348  psss  14573  mhmeql  14691  gsumvallem1  14698  frmdss2  14735  frmdup3  14738  grprcan  14765  mulgnn0ass  14846  isnsg3  14901  ghmpreima  14954  ghmeql  14955  gaorber  15012  oddvds  15112  gexdvds  15145  sylow1lem1  15159  odcau  15165  pgpssslw  15175  sylow2alem2  15179  sylow2blem3  15183  fislw  15186  sylow2  15187  lsmmod  15234  efgredlem  15306  frgpup3  15337  gexex  15395  gsumval3  15441  gsumzres  15444  gsumzcl  15445  gsumzf1o  15446  gsumzaddlem  15453  gsumconst  15459  gsumzmhm  15460  gsumzoppg  15466  gsum2d2lem  15474  ablfac1eulem  15557  pgpfac1lem5  15564  ablfaclem3  15572  issubdrg  15820  lss1d  15966  lmhmeql  16058  lspextmo  16059  lspsnat  16144  lsppratlem6  16151  islbs3  16154  lbsextlem4  16160  lidl1el  16216  mvrf1  16416  mplsubglem  16425  mpllsslem  16426  mplcoe1  16455  mplcoe2  16457  cnsubrg  16682  gsumfsum  16689  prmirredlem  16696  znidomb  16765  frgpcyg  16777  cssmre  16843  en2top  16973  toponmre  17080  topssnei  17111  innei  17112  clslp  17134  restcls  17167  restntr  17168  ordtrest2lem  17189  cnpco  17253  cncls2  17259  cncnpi  17264  cncnp  17266  cnconst2  17269  cnpdis  17279  lmcnp  17290  cnhaus  17340  nrmsep  17343  regsep2  17362  isreg2  17363  cncmp  17377  tgcmp  17386  sscmp  17390  cmpfi  17393  cnconn  17406  iunconlem  17411  clscon  17414  1stcfb  17429  1stcrest  17437  2ndcctbss  17439  2ndcdisj  17440  1stcelcls  17445  1stccnp  17446  restnlly  17466  cldllycmp  17479  lly1stc  17480  dislly  17481  kgentopon  17491  kgenidm  17500  1stckgenlem  17506  kgencn3  17511  ptpjpre1  17524  ptbasin  17530  txcls  17557  tx2cn  17563  ptpjcn  17564  ptclsg  17568  ptcnp  17575  txdis  17585  txlly  17589  txnlly  17590  pthaus  17591  txtube  17593  txcmplem1  17594  txcmplem2  17595  txcmp  17596  txhaus  17600  txkgen  17605  xkohaus  17606  xkococnlem  17612  xkococn  17613  txcon  17642  qtopeu  17669  qtoprest  17670  regr1lem2  17693  kqreglem1  17694  cmphaushmeo  17753  xkocnv  17767  fgabs  17832  filuni  17838  trufil  17863  ufileu  17872  filufint  17873  fin1aufil  17885  elfm2  17901  rnelfmlem  17905  fmfnfmlem2  17908  fmfnfmlem4  17910  fmufil  17912  flimopn  17928  fbflim2  17930  hausflimi  17933  hausflim  17934  flimcf  17935  flimclslem  17937  flimsncls  17939  hauspwpwf1  17940  cnpflfi  17952  fclsnei  17972  fclscf  17978  flimfnfcls  17981  fclscmp  17983  ufilcmp  17985  fcfnei  17988  cnpfcf  17994  alexsublem  17996  alexsub  17997  alexsubALTlem2  18000  alexsubALTlem3  18001  alexsubALTlem4  18002  ptcmplem3  18006  ptcmplem4  18007  ptcmplem5  18008  symgtgp  18052  tgpconcompeqg  18062  tgpconcomp  18063  ghmcnp  18065  tgpt0  18069  divstgplem  18071  haustsms2  18087  tsmsgsum  18089  tsmsres  18094  tsmsxp  18105  imasdsf1olem  18311  xbln0  18339  blss  18346  neibl  18421  blcld  18425  metss  18428  metequiv2  18430  met1stc  18441  metrest  18444  prdsxmslem2  18449  metcnp3  18460  nrmmetd  18493  nlmvscnlem1  18593  nrginvrcnlem  18597  nmoleub  18636  icccmplem2  18725  icccmp  18727  reconnlem2  18729  xrge0tsms  18736  metdstri  18752  metdseq0  18755  metdscn  18757  cnmpt2pc  18824  cnheibor  18851  lebnumlem3  18859  pcoval2  18912  pcopt  18918  nmoleub2lem  18993  nmhmcn  18999  ipcnlem1  19070  cfilfcls  19098  cmetcaulem  19112  iscmet3lem2  19116  iscmet3  19117  equivcau  19124  caubl  19131  lmcau  19136  bcthlem2  19147  bcthlem3  19148  bcthlem4  19149  bcthlem5  19150  ivthlem2  19216  ivthlem3  19217  ovoliunlem2  19266  ovolicc2lem2  19281  ovolicc2lem3  19282  ovolicc2lem5  19284  ovolicc2  19285  ismbl2  19290  nulmbl  19297  nulmbl2  19298  unmbl  19299  shftmbl  19300  voliunlem3  19313  volsup  19317  ioombl1lem4  19322  ioombl1  19323  icombl  19325  ioombl  19326  uniioombl  19348  opnmbllem  19360  volivth  19366  vitali  19372  ismbf3d  19413  mbflimsup  19425  i1fadd  19454  itg1addlem4  19458  itg2le  19498  itg2seq  19501  itg2lea  19503  itg2splitlem  19507  itg2split  19508  itg2mono  19512  itg2gt0  19519  itg2cnlem2  19521  itgss  19570  itgfsum  19585  itgcn  19601  ellimc3  19633  limcco  19647  limciun  19648  dvnres  19684  dvnfre  19705  rolle  19741  c1liplem1  19747  dvivth  19761  dvne0  19762  lhop1lem  19764  lhop1  19765  lhop  19767  dvcnvrelem1  19768  dvfsumrlim  19782  dvfsum2  19785  ftc1a  19788  ftc1lem6  19792  itgsubst  19800  tdeglem4  19850  mdegaddle  19864  mdegvscale  19865  mdegmullem  19868  deg1tmle  19907  ply1divex  19926  dvdsq1p  19950  fta1g  19957  fta1b  19959  plyco0  19978  coeeulem  20010  dgrlem  20015  plyco  20027  coemullem  20035  dgreq0  20050  dgrco  20060  plydivex  20081  quotcan  20093  aannenlem1  20112  aalioulem2  20117  aalioulem3  20118  taylthlem1  20156  ulmbdd  20181  ulmdvlem3  20185  itgulm  20191  radcnvlt1  20201  psercnlem1  20208  abelthlem2  20215  abelthlem8  20222  logcnlem5  20404  efopn  20416  cxpmul2z  20449  cxpcn3lem  20498  cxpeq  20508  xrlimcnp  20674  cxplim  20677  o1cxp  20680  cxploglim  20683  scvxcvx  20691  jensen  20694  ftalem1  20722  ftalem2  20723  fta  20729  basellem3  20732  isppw2  20765  ppinprm  20802  chtnprm  20804  dvdsmulf1o  20846  chtublem  20862  perfectlem2  20881  dchrfi  20906  dchrptlem1  20915  dchrptlem2  20916  dchrptlem3  20917  dchrsum2  20919  bposlem1  20935  bposlem3  20937  2sqlem5  21019  2sqlem6  21020  2sqlem8  21023  2sqlem10  21025  2sqb  21029  chebbnd1lem1  21030  chtppilimlem2  21035  dchrisum0flb  21071  dchrisum0fno1  21072  dchrisum0  21081  pntrsumbnd2  21128  pntpbnd1  21147  pntpbnd2  21148  pntlemp  21171  pnt3  21173  qabvle  21186  ostth2lem2  21195  ostth3  21199  ostth  21200  umgraex  21225  eupai  21537  isgrp2d  21671  ghgrp  21804  ghablo  21805  smcnlem  22041  ubthlem1  22220  ubthlem3  22222  htthlem  22268  pjhthlem2  22742  5oalem6  23009  leopmuli  23484  pjnormssi  23519  pjclem4  23550  pj3si  23558  hatomistici  23713  sumdmdlem  23769  reximddv  23806  suppss2f  23892  xrge0tsmsd  24052  qqhf  24169  ballotlemfc0  24529  ballotlemfcc  24530  subfacp1lem5  24649  erdszelem7  24662  erdszelem11  24666  pconcon  24697  txpcon  24698  conpcon  24701  sconpi1  24705  txscon  24707  cvxscon  24709  cvmopnlem  24744  cvmfolem  24745  cvmliftmolem2  24748  cvmliftlem7  24757  cvmliftlem10  24760  cvmliftlem15  24764  cvmlift2lem10  24778  cvmlift3lem4  24788  cvmlift3lem8  24792  dedekind  24966  dedekindle  24967  mulge0b  24970  prodmolem2  25040  zprod  25042  fprod  25046  fprodf1o  25051  prodss  25052  fprodss  25053  fprodcl2lem  25055  fprodmul  25063  fproddiv  25064  fprodconst  25081  fprodn0  25082  nofulllem4  25383  colinearalglem4  25562  axcontlem10  25626  btwnouttr2  25670  cgrxfr  25703  btwnxfr  25704  brcolinear  25707  lineext  25724  btwnconn1lem13  25747  midofsegid  25752  segcon2  25753  brsegle  25756  seglecgr12im  25758  segletr  25762  colinbtwnle  25766  broutsideof2  25770  btwnoutside  25773  broutsideof3  25774  outsideoftr  25777  outsideofeq  25778  outsideofeu  25779  outsidele  25780  lineunray  25795  lineelsb2  25796  linethru  25801  supaddc  25947  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  itg2addnclem  25957  ftc1cnnc  25979  finminlem  26012  nn0prpwlem  26016  locfincmp  26075  comppfsc  26078  neibastop2lem  26080  neibastop2  26081  neibastop3  26082  topjoin  26085  tailfb  26097  sdclem2  26137  fdc  26140  istotbnd3  26171  isbnd2  26183  isbnd3  26184  prdsbnd  26193  cntotbnd  26196  heibor1lem  26209  heibor1  26210  heiborlem10  26220  rrncmslem  26232  ghomco  26249  1idl  26327  unichnidl  26332  prtlem10  26405  prtlem18  26417  isnacs3  26455  nacsfix  26457  fnwe2lem2  26817  kelac1  26830  dsmmsubg  26878  dsmmlss  26879  frlmsslsp  26917  unxpwdom3  26925  enfixsn  26926  lindff1  26959  lindfrn  26960  hbtlem5  27001  hbt  27003  dgraa0p  27023  f1omvdco2  27060  psgnunilem1  27085  psgnunilem2  27087  hashgcdeq  27186  rlimdmafv  27710  atlatmstc  29434  cvrexchlem  29533  paddasslem14  29947  pexmidlem5N  30088  cdleme29ex  30488  cdlemefr29exN  30516  cdleme32fva  30551  diarnN  31244  dihlsscpre  31349
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator