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  2791  disjxiun  4169  wereu2  4539  suppss  5822  fcof1  5979  knatar  6039  ovmpt2df  6164  suppss2  6259  riota5f  6533  smoord  6586  tfrlem9a  6606  oaass  6763  oelimcl  6802  oaabs2  6847  swoso  6895  eceqoveq  6968  domdifsn  7150  domunsncan  7167  omxpenlem  7168  mapdom2  7237  frfi  7311  fofinf1o  7346  finsschain  7371  elfiun  7393  marypha1lem  7396  eqsupd  7418  ordiso2  7440  ordtypelem6  7448  ordtypelem7  7449  ordtypelem10  7452  oismo  7465  wemapso2lem  7475  brwdom2  7497  wdomtr  7499  unwdomg  7508  xpwdomg  7509  unxpwdom2  7512  cantnfval2  7580  cantnfle  7582  cantnfreslem  7587  cantnflem1  7601  cantnf  7605  r1ordg  7660  tcrank  7764  carddomi2  7813  harval2  7840  infxpenlem  7851  infxpenc2lem2  7857  fseqenlem1  7861  dfac8clem  7869  acndom2  7891  infpwfien  7899  iunfictbso  7951  dfac12lem3  7981  infxp  8051  coflim  8097  cofsmo  8105  coftr  8109  sornom  8113  infpssrlem4  8142  enfin2i  8157  fin23lem26  8161  fin23lem27  8164  fin23lem36  8184  fin23lem40  8187  isf32lem5  8193  isf34lem4  8213  isfin1-3  8222  fin1a2lem10  8245  fin1a2lem13  8248  fin1a2s  8250  hsmexlem4  8265  ttukeylem5  8349  ttukeylem6  8350  ttukeylem7  8351  alephval2  8403  gchor  8458  fpwwe2lem7  8467  fpwwe2lem12  8472  fpwwe2  8474  pwfseqlem4a  8492  pwfseqlem4  8493  winalim2  8527  gchina  8530  inar1  8606  nqereq  8768  prlem934  8866  prlem936  8880  supsrlem  8942  axpre-sup  9000  prodge0  9813  supmul1  9929  un0addcl  10209  un0mulcl  10210  uzwo3  10525  qbtwnre  10741  xlemul1a  10823  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqf1olem1  11317  seqid2  11324  seqhomo  11325  expnegz  11369  expcan  11387  ltexp2  11388  discr  11471  bcval5  11564  hashbc  11657  hashf1lem2  11660  seqcoll  11667  seqcoll2  11668  wrdind  11746  cau3lem  12113  ello1d  12272  lo1bdd2  12273  rlimclim  12295  climrlim2  12296  rlimdm  12300  rlimcn1  12337  reccn2  12345  rlimsqzlem  12397  lo1le  12400  caucvgrlem  12421  caurcvg2  12426  summolem2  12465  zsum  12467  fsum  12469  fsumf1o  12472  sumss  12473  fsumss  12474  fsumcl2lem  12480  fsumadd  12487  fsumcom2  12513  fsum0diag2  12521  fsummulc2  12522  fsumconst  12528  fsumrelem  12541  fsumrlim  12545  fsumo1  12546  divrcnv  12587  geomulcvg  12608  mertenslem2  12617  ruclem8  12791  dvds0lem  12815  dvdsnegb  12822  dvdssub2  12842  bitsf1  12913  bitsshft  12942  bezoutlem3  12995  bezoutlem4  12996  isprm2lem  13041  isprm6  13064  isprm5  13067  pcqmul  13182  pcqcl  13185  pcxcl  13189  pc2dvds  13207  pcadd  13213  pcmpt  13216  pockthg  13229  infpnlem1  13233  prmreclem5  13243  vdwlem2  13305  vdwlem9  13312  vdwlem10  13313  vdwlem12  13315  ramub  13336  0ram  13343  ramub1lem2  13350  ramub1  13351  ramcl  13352  mreexexd  13828  acsfn2  13843  iscatd  13853  catpropd  13890  setcmon  14197  drsdirfi  14350  pleval2i  14376  psss  14601  mhmeql  14719  gsumvallem1  14726  frmdss2  14763  frmdup3  14766  grprcan  14793  mulgnn0ass  14874  isnsg3  14929  ghmpreima  14982  ghmeql  14983  gaorber  15040  oddvds  15140  gexdvds  15173  sylow1lem1  15187  odcau  15193  pgpssslw  15203  sylow2alem2  15207  sylow2blem3  15211  fislw  15214  sylow2  15215  lsmmod  15262  efgredlem  15334  frgpup3  15365  gexex  15423  gsumval3  15469  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  gsum2d2lem  15502  ablfac1eulem  15585  pgpfac1lem5  15592  ablfaclem3  15600  issubdrg  15848  lss1d  15994  lmhmeql  16086  lspextmo  16087  lspsnat  16172  lsppratlem6  16179  islbs3  16182  lbsextlem4  16188  lidl1el  16244  mvrf1  16444  mplsubglem  16453  mpllsslem  16454  mplcoe1  16483  mplcoe2  16485  cnsubrg  16714  gsumfsum  16721  prmirredlem  16728  znidomb  16797  frgpcyg  16809  cssmre  16875  en2top  17005  toponmre  17112  topssnei  17143  innei  17144  clslp  17166  restcls  17199  restntr  17200  ordtrest2lem  17221  cnpco  17285  cncls2  17291  cncnpi  17296  cncnp  17298  cnconst2  17301  cnpdis  17311  lmcnp  17322  cnhaus  17372  nrmsep  17375  regsep2  17394  isreg2  17395  cncmp  17409  tgcmp  17418  sscmp  17422  cmpfi  17425  cnconn  17438  iunconlem  17443  clscon  17446  1stcfb  17461  1stcrest  17469  2ndcctbss  17471  2ndcdisj  17472  1stcelcls  17477  1stccnp  17478  restnlly  17498  cldllycmp  17511  lly1stc  17512  dislly  17513  kgentopon  17523  kgenidm  17532  1stckgenlem  17538  kgencn3  17543  ptpjpre1  17556  ptbasin  17562  txcls  17589  tx2cn  17595  ptpjcn  17596  ptclsg  17600  ptcnp  17607  txdis  17617  txlly  17621  txnlly  17622  pthaus  17623  txtube  17625  txcmplem1  17626  txcmplem2  17627  txcmp  17628  txhaus  17632  txkgen  17637  xkohaus  17638  xkococnlem  17644  xkococn  17645  txcon  17674  qtopeu  17701  qtoprest  17702  regr1lem2  17725  kqreglem1  17726  cmphaushmeo  17785  xkocnv  17799  fgabs  17864  filuni  17870  trufil  17895  ufileu  17904  filufint  17905  fin1aufil  17917  elfm2  17933  rnelfmlem  17937  fmfnfmlem2  17940  fmfnfmlem4  17942  fmufil  17944  flimopn  17960  fbflim2  17962  hausflimi  17965  hausflim  17966  flimcf  17967  flimclslem  17969  flimsncls  17971  hauspwpwf1  17972  cnpflfi  17984  fclsnei  18004  fclscf  18010  flimfnfcls  18013  fclscmp  18015  ufilcmp  18017  fcfnei  18020  cnpfcf  18026  alexsublem  18028  alexsub  18029  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem3  18038  ptcmplem4  18039  ptcmplem5  18040  symgtgp  18084  tgpconcompeqg  18094  tgpconcomp  18095  ghmcnp  18097  tgpt0  18101  divstgplem  18103  haustsms2  18119  tsmsgsum  18121  tsmsres  18126  tsmsxp  18137  imasdsf1olem  18356  xbln0  18397  blssps  18407  blss  18408  neibl  18484  blcld  18488  metss  18491  metequiv2  18493  met1stc  18504  metrest  18507  prdsxmslem2  18512  metcnp3  18523  nrmmetd  18575  nlmvscnlem1  18675  nrginvrcnlem  18679  nmoleub  18718  icccmplem2  18807  icccmp  18809  reconnlem2  18811  xrge0tsms  18818  metdstri  18834  metdseq0  18837  metdscn  18839  cnmpt2pc  18906  cnheibor  18933  lebnumlem3  18941  pcoval2  18994  pcopt  19000  nmoleub2lem  19075  nmhmcn  19081  ipcnlem1  19152  cfilfcls  19180  cmetcaulem  19194  iscmet3lem2  19198  iscmet3  19199  equivcau  19206  caubl  19213  lmcau  19218  bcthlem2  19231  bcthlem3  19232  bcthlem4  19233  bcthlem5  19234  ivthlem2  19302  ivthlem3  19303  ovoliunlem2  19352  ovolicc2lem2  19367  ovolicc2lem3  19368  ovolicc2lem5  19370  ovolicc2  19371  ismbl2  19376  nulmbl  19383  nulmbl2  19384  unmbl  19385  shftmbl  19386  voliunlem3  19399  volsup  19403  ioombl1lem4  19408  ioombl1  19409  icombl  19411  ioombl  19412  uniioombl  19434  opnmbllem  19446  volivth  19452  vitali  19458  ismbf3d  19499  mbflimsup  19511  i1fadd  19540  itg1addlem4  19544  itg2le  19584  itg2seq  19587  itg2lea  19589  itg2splitlem  19593  itg2split  19594  itg2mono  19598  itg2gt0  19605  itg2cnlem2  19607  itgss  19656  itgfsum  19671  itgcn  19687  ellimc3  19719  limcco  19733  limciun  19734  dvnres  19770  dvnfre  19791  rolle  19827  c1liplem1  19833  dvivth  19847  dvne0  19848  lhop1lem  19850  lhop1  19851  lhop  19853  dvcnvrelem1  19854  dvfsumrlim  19868  dvfsum2  19871  ftc1a  19874  ftc1lem6  19878  itgsubst  19886  tdeglem4  19936  mdegaddle  19950  mdegvscale  19951  mdegmullem  19954  deg1tmle  19993  ply1divex  20012  dvdsq1p  20036  fta1g  20043  fta1b  20045  plyco0  20064  coeeulem  20096  dgrlem  20101  plyco  20113  coemullem  20121  dgreq0  20136  dgrco  20146  plydivex  20167  quotcan  20179  aannenlem1  20198  aalioulem2  20203  aalioulem3  20204  taylthlem1  20242  ulmbdd  20267  ulmdvlem3  20271  itgulm  20277  radcnvlt1  20287  psercnlem1  20294  abelthlem2  20301  abelthlem8  20308  logcnlem5  20490  efopn  20502  cxpmul2z  20535  cxpcn3lem  20584  cxpeq  20594  xrlimcnp  20760  cxplim  20763  o1cxp  20766  cxploglim  20769  scvxcvx  20777  jensen  20780  ftalem1  20808  ftalem2  20809  fta  20815  basellem3  20818  isppw2  20851  ppinprm  20888  chtnprm  20890  dvdsmulf1o  20932  chtublem  20948  perfectlem2  20967  dchrfi  20992  dchrptlem1  21001  dchrptlem2  21002  dchrptlem3  21003  dchrsum2  21005  bposlem1  21021  bposlem3  21023  2sqlem5  21105  2sqlem6  21106  2sqlem8  21109  2sqlem10  21111  2sqb  21115  chebbnd1lem1  21116  chtppilimlem2  21121  dchrisum0flb  21157  dchrisum0fno1  21158  dchrisum0  21167  pntrsumbnd2  21214  pntpbnd1  21233  pntpbnd2  21234  pntlemp  21257  pnt3  21259  qabvle  21272  ostth2lem2  21281  ostth3  21285  ostth  21286  umgraex  21311  eupai  21642  isgrp2d  21776  ghgrp  21909  ghablo  21910  smcnlem  22146  ubthlem1  22325  ubthlem3  22327  htthlem  22373  pjhthlem2  22847  5oalem6  23114  leopmuli  23589  pjnormssi  23624  pjclem4  23655  pj3si  23663  hatomistici  23818  sumdmdlem  23874  reximddv  23915  suppss2f  24002  xrge0tsmsd  24176  qqhf  24323  ballotlemfc0  24703  ballotlemfcc  24704  subfacp1lem5  24823  erdszelem7  24836  erdszelem11  24840  pconcon  24871  txpcon  24872  conpcon  24875  sconpi1  24879  txscon  24881  cvxscon  24883  cvmopnlem  24918  cvmfolem  24919  cvmliftmolem2  24922  cvmliftlem7  24931  cvmliftlem10  24934  cvmliftlem15  24938  cvmlift2lem10  24952  cvmlift3lem4  24962  cvmlift3lem8  24966  dedekind  25140  dedekindle  25141  mulge0b  25144  prodmolem2  25214  zprod  25216  fprod  25220  fprodf1o  25225  prodss  25226  fprodss  25227  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodconst  25255  fprodn0  25256  fprodcom2  25261  nofulllem4  25573  colinearalglem4  25752  axcontlem10  25816  btwnouttr2  25860  cgrxfr  25893  btwnxfr  25894  brcolinear  25897  lineext  25914  btwnconn1lem13  25937  midofsegid  25942  segcon2  25943  brsegle  25946  seglecgr12im  25948  segletr  25952  colinbtwnle  25956  broutsideof2  25960  btwnoutside  25963  broutsideof3  25964  outsideoftr  25967  outsideofeq  25968  outsideofeu  25969  outsidele  25970  lineunray  25985  lineelsb2  25986  linethru  25991  supaddc  26137  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  itg2addnclem  26155  itg2addnclem3  26157  ftc1cnnc  26178  finminlem  26211  nn0prpwlem  26215  locfincmp  26274  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  neibastop3  26281  topjoin  26284  tailfb  26296  sdclem2  26336  fdc  26339  istotbnd3  26370  isbnd2  26382  isbnd3  26383  prdsbnd  26392  cntotbnd  26395  heibor1lem  26408  heibor1  26409  heiborlem10  26419  rrncmslem  26431  ghomco  26448  1idl  26526  unichnidl  26531  prtlem10  26604  prtlem18  26616  isnacs3  26654  nacsfix  26656  fnwe2lem2  27016  kelac1  27029  dsmmsubg  27077  dsmmlss  27078  frlmsslsp  27116  unxpwdom3  27124  enfixsn  27125  lindff1  27158  lindfrn  27159  hbtlem5  27200  hbt  27202  dgraa0p  27222  f1omvdco2  27259  psgnunilem1  27284  psgnunilem2  27286  hashgcdeq  27385  rlimdmafv  27908  atlatmstc  29802  cvrexchlem  29901  paddasslem14  30315  pexmidlem5N  30456  cdleme29ex  30856  cdlemefr29exN  30884  cdleme32fva  30919  diarnN  31612  dihlsscpre  31717
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