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

Theorem expr 598
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 588 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  rexlimdvaa  2681  disjxiun  4036  wereu2  4406  suppss  5674  fcof1  5813  knatar  5873  ovmpt2df  5995  grprinvlem  6074  grpridd  6076  suppss2  6089  riota5f  6345  smoord  6398  tfrlem9a  6418  oaass  6575  oelimcl  6614  nnawordex  6651  oaabs2  6659  swoso  6707  eceqoveq  6779  domdifsn  6961  domunsncan  6978  omxpenlem  6979  mapdom2  7048  frfi  7118  fofinf1o  7153  finsschain  7178  fiin  7191  elfiun  7199  marypha1lem  7202  eqsupd  7224  ordiso2  7246  ordtypelem6  7254  ordtypelem7  7255  ordtypelem10  7258  oismo  7271  wemaplem3  7279  wemapso2lem  7281  brwdom2  7303  wdomtr  7305  unwdomg  7314  xpwdomg  7315  unxpwdom2  7318  cantnfval2  7386  cantnfle  7388  cantnflt  7389  cantnfreslem  7393  oemapvali  7402  cantnflem1  7407  cantnflem4  7410  cantnf  7411  r1ordg  7466  r1pwss  7472  tcrank  7570  carddomi2  7619  harval2  7646  infxpenlem  7657  infxpenc2lem1  7662  infxpenc2lem2  7663  fseqenlem1  7667  fseqenlem2  7668  dfac8clem  7675  acndom2  7697  infpwfien  7705  iunfictbso  7757  dfac12lem3  7787  infxp  7857  coflim  7903  cofsmo  7911  coftr  7915  sornom  7919  infpssrlem4  7948  enfin2i  7963  fin23lem26  7967  fin23lem27  7970  fin23lem36  7990  fin23lem40  7993  isf32lem5  7999  isf34lem4  8019  isfin1-3  8028  fin1a2lem10  8051  fin1a2lem13  8054  fin1a2s  8056  hsmexlem4  8071  ttukeylem5  8156  ttukeylem6  8157  ttukeylem7  8158  alephval2  8210  gchor  8265  fpwwe2lem7  8274  fpwwe2lem12  8279  fpwwe2  8281  pwfseqlem3  8298  pwfseqlem4a  8299  pwfseqlem4  8300  winalim2  8334  gchina  8337  r1wunlim  8375  wunex2  8376  inttsk  8412  inar1  8413  nqereq  8575  prlem934  8673  prlem936  8687  supsrlem  8749  axpre-sup  8807  addcan  9012  addcan2  9013  negeu  9058  mulcand  9417  prodge0  9619  supmul1  9735  un0addcl  10013  un0mulcl  10014  suprzcl  10107  zsupss  10323  uzwo3  10327  qbtwnre  10542  xralrple  10548  xlemul1a  10624  seqcl2  11080  seqfveq2  11084  seqshft2  11088  monoord  11092  seqsplit  11095  seqf1olem1  11101  seqid2  11108  seqhomo  11109  expnegz  11152  expcan  11170  ltexp2  11171  expmulnbnd  11249  discr  11254  bcval5  11346  hashbc  11407  hashf1lem2  11410  seqcoll  11417  seqcoll2  11418  wrdind  11493  rexanuz  11845  cau3lem  11854  limsupval2  11970  limsupgre  11971  ello1d  12013  lo1bdd2  12014  rlimclim1  12035  rlimclim  12036  climrlim2  12037  rlimdm  12041  rlimcn1  12078  reccn2  12086  rlimsqzlem  12138  lo1le  12141  caucvgrlem  12161  caurcvg2  12166  summolem2  12205  zsum  12207  fsum  12209  fsumf1o  12212  sumss  12213  fsumss  12214  fsumcvg3  12218  fsumcl2lem  12220  fsumadd  12227  fsumcom2  12253  fsum0diag2  12261  fsummulc2  12262  fsumconst  12268  fsumrelem  12281  fsumrlim  12285  fsumo1  12286  divrcnv  12327  geomulcvg  12348  mertenslem2  12357  rpnnen2  12520  ruclem8  12531  dvds0lem  12555  dvdsnegb  12562  dvdssub2  12582  oexpneg  12606  bitsfi  12644  bitsf1  12653  bitsshft  12682  bezoutlem3  12735  bezoutlem4  12736  isprm2lem  12781  prmind2  12785  isprm6  12804  isprm5  12807  pcqmul  12922  pcqcl  12925  pcxcl  12929  pc2dvds  12947  pcprmpw2  12950  pcadd  12953  pcmpt  12956  pockthg  12969  infpnlem1  12973  prmreclem5  12983  vdwlem2  13045  vdwlem6  13049  vdwlem9  13052  vdwlem10  13053  vdwlem12  13055  ramub  13076  0ram  13083  ramub1lem2  13090  ramub1  13091  ramcl  13092  mreexexd  13566  acsfn2  13581  iscatd  13591  catpropd  13628  setcmon  13935  drsdirfi  14088  pleval2i  14114  psss  14339  mhmeql  14457  gsumvallem1  14464  frmdss2  14501  frmdup3  14504  grprcan  14531  mulgnn0ass  14612  isnsg3  14667  ghmpreima  14720  ghmeql  14721  gaorber  14778  oddvds  14878  gexdvds  14911  sylow1lem1  14925  sylow1  14930  odcau  14931  pgpfi  14932  pgpssslw  14941  sylow2alem2  14945  sylow2blem3  14949  slwhash  14951  fislw  14952  sylow2  14953  sylow3lem2  14955  lsmmod  15000  pj1id  15024  efgsfo  15064  efgredlemc  15070  efgredlem  15072  frgpup3  15103  gexex  15161  lt6abl  15197  ghmcyg  15198  gsumval3  15207  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsumzoppg  15232  gsum2d2lem  15240  dmdprdsplitlem  15288  dpjidcl  15309  ablfac1eulem  15323  pgpfac1lem4  15329  pgpfac1lem5  15330  pgpfaclem2  15333  pgpfaclem3  15334  ablfaclem3  15338  unitgrp  15465  irredrmul  15505  issubdrg  15586  lss1d  15736  lmhmeql  15828  lspextmo  15829  lspsolv  15912  lspsnat  15914  lsppratlem6  15921  islbs3  15924  lbsextlem4  15930  lidl1el  15986  mvrf1  16186  mplsubglem  16195  mpllsslem  16196  mplcoe1  16225  mplcoe2  16227  cnsubrg  16448  gsumfsum  16455  prmirredlem  16462  znidomb  16531  znunit  16533  frgpcyg  16543  cssmre  16609  en2top  16739  toponmre  16846  neiint  16857  topssnei  16877  innei  16878  clslp  16895  restbas  16905  restopnb  16922  restcls  16927  restntr  16928  ordtrest2lem  16949  pnfnei  16966  mnfnei  16967  cnpco  17012  cncls2  17018  cncnpi  17023  cncnp  17025  cnconst2  17027  cnpdis  17037  lmcnp  17048  pnrmopn  17087  haust1  17096  cnhaus  17098  nrmsep  17101  regsep2  17120  isreg2  17121  ordthauslem  17127  cncmp  17135  tgcmp  17144  sscmp  17148  cmpfi  17151  cnconn  17164  iunconlem  17169  clscon  17172  t1conperf  17178  1stcfb  17187  1stcrest  17195  2ndcctbss  17197  2ndcdisj  17198  2ndcomap  17200  dis2ndc  17202  1stcelcls  17203  1stccnp  17204  restnlly  17224  islly2  17226  nllyrest  17228  llyidm  17230  nllyidm  17231  hausllycmp  17236  cldllycmp  17237  lly1stc  17238  dislly  17239  kgentopon  17249  kgenidm  17258  llycmpkgen2  17261  1stckgenlem  17264  kgencn3  17269  ptpjpre1  17282  ptbasin  17288  ptbasfi  17292  txcls  17315  tx2cn  17320  ptpjcn  17321  ptclsg  17325  ptcnp  17332  txdis  17342  txlly  17346  txnlly  17347  pthaus  17348  txtube  17350  txcmplem1  17351  txcmplem2  17352  txcmp  17353  txhaus  17357  txkgen  17362  xkohaus  17363  xkococnlem  17369  xkococn  17370  txcon  17399  basqtop  17418  tgqtop  17419  qtopeu  17423  qtoprest  17424  regr1lem  17446  regr1lem2  17447  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  reghmph  17500  nrmhmph  17501  cmphaushmeo  17507  xkocnv  17521  qtophmeo  17524  fbssfi  17548  trfbas2  17554  fgabs  17590  neifil  17591  filuni  17596  trfil2  17598  trfg  17602  trufil  17621  ssufl  17629  ufileu  17630  filufint  17631  fin1aufil  17643  elfm2  17659  rnelfmlem  17663  fmfnfmlem2  17666  fmfnfmlem4  17668  fmufil  17670  ufldom  17673  flimopn  17686  fbflim2  17688  hausflimi  17691  hausflim  17692  flimcf  17693  flimclslem  17695  flimsncls  17697  hauspwpwf1  17698  cnpflfi  17710  fclsnei  17730  fclscf  17736  fclsfnflim  17738  flimfnfcls  17739  fclscmp  17741  uffclsflim  17742  ufilcmp  17743  fcfnei  17746  cnpfcfi  17751  cnpfcf  17752  alexsublem  17754  alexsub  17755  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem3  17764  ptcmplem4  17765  ptcmplem5  17766  symgtgp  17800  tgpconcompeqg  17810  tgpconcomp  17811  ghmcnp  17813  tgpt0  17817  divstgplem  17819  haustsms2  17835  tsmsgsum  17837  tsmsres  17842  tsmsxp  17853  imasdsf1olem  17953  xbln0  17981  blss  17988  blssex  17989  neibl  18063  blcld  18067  metss  18070  metequiv2  18072  met1stc  18083  met2ndci  18084  metrest  18086  prdsxmslem2  18091  metcnp3  18102  metcnpi3  18108  nrmmetd  18113  nlmvscnlem1  18213  nrginvrcnlem  18217  nmoleub  18256  icccmplem1  18343  icccmplem2  18344  icccmplem3  18345  icccmp  18346  reconnlem2  18348  xrge0tsms  18355  metdstri  18371  metdseq0  18374  metdscn  18376  cnmpt2pc  18442  cnheibor  18469  cnllycmp  18470  bndth  18472  lebnumlem1  18475  lebnumlem3  18477  lebnum  18478  pcoval2  18530  pcopt  18536  pi1blem  18553  nmoleub2lem  18611  nmhmcn  18617  ipcnlem1  18688  iscfil3  18715  cfilfcls  18716  cmetcaulem  18730  iscmet3lem2  18734  iscmet3  18735  equivcau  18742  lmle  18743  caubl  18749  lmcau  18754  cmetss  18756  relcmpcmet  18758  bcthlem2  18763  bcthlem3  18764  bcthlem4  18765  bcthlem5  18766  pjthlem2  18818  ivthlem2  18828  ivthlem3  18829  ovoliunlem2  18878  ovolscalem2  18889  ovolicc2lem2  18893  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2lem5  18896  ovolicc2  18897  ismbl2  18902  nulmbl  18909  nulmbl2  18910  unmbl  18911  shftmbl  18912  voliunlem3  18925  volsup  18929  ioombl1lem4  18934  ioombl1  18935  icombl  18937  ioombl  18938  uniioombllem6  18959  uniioombl  18960  dyadmbllem  18970  opnmbllem  18972  volivth  18978  vitali  18984  ismbf3d  19025  mbfinf  19036  mbflimsup  19037  i1fadd  19066  itg1addlem4  19070  mbfi1fseqlem6  19091  itg2le  19110  itg2const2  19112  itg2seq  19113  itg2lea  19115  itg2splitlem  19119  itg2split  19120  itg2mono  19124  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  itgss  19182  itgfsum  19197  bddmulibl  19209  itgcn  19213  ellimc3  19245  limcflf  19247  limcco  19259  limciun  19260  dvnres  19296  dvnfre  19317  rolle  19353  c1liplem1  19359  dvivth  19373  dvne0  19374  lhop1lem  19376  lhop1  19377  lhop2  19378  lhop  19379  dvcnvrelem1  19380  dvcnvre  19382  dvfsumrlim  19394  dvfsum2  19397  ftc1a  19400  ftc1lem6  19404  itgsubst  19412  tdeglem4  19462  mdegaddle  19476  mdegvscale  19477  mdegmullem  19480  deg1tmle  19519  ply1divex  19538  dvdsq1p  19562  fta1g  19569  fta1b  19571  plyco0  19590  coeeulem  19622  dgrlem  19627  plyco  19639  coemullem  19647  dgreq0  19662  dgrco  19672  plydivex  19693  quotcan  19705  aareccl  19722  aannenlem1  19724  aalioulem2  19729  aalioulem3  19730  taylthlem1  19768  ulmbdd  19791  ulmdvlem3  19795  iblulm  19799  itgulm  19800  radcnvlem1  19805  radcnvlt1  19810  psercnlem1  19817  abelthlem2  19824  abelthlem5  19827  abelthlem8  19831  logcnlem5  20009  efopn  20021  cxpmul2z  20054  cxpcn3lem  20103  cxpeq  20113  dcubic  20158  xrlimcnp  20279  cxplim  20282  o1cxp  20285  cxploglim  20288  scvxcvx  20296  jensen  20299  amgm  20301  ftalem1  20326  ftalem2  20327  fta  20333  basellem3  20336  isppw2  20369  ppinprm  20406  chtnprm  20408  dvdsmulf1o  20450  chtublem  20466  perfectlem2  20485  dchrfi  20510  dchrptlem1  20519  dchrptlem2  20520  dchrptlem3  20521  dchrsum2  20523  sumdchr2  20525  bposlem1  20539  bposlem3  20541  lgsne0  20588  lgsqr  20601  lgsquadlem1  20609  2sqlem5  20623  2sqlem6  20624  2sqlem8  20627  2sqlem10  20629  2sqlem11  20630  2sqb  20633  chebbnd1lem1  20634  chtppilimlem2  20639  dchrisum  20657  dchrvmasumif  20668  dchrisum0flb  20675  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem3  20684  dchrisum0  20685  dchrmusum  20689  dchrvmasum  20690  chpdifbnd  20720  pntrsumbnd2  20732  pntrlog2bnd  20749  pntpbnd1  20751  pntpbnd2  20752  pntibndlem3  20757  pntibnd  20758  pntlemi  20769  pntlemp  20775  pntleml  20776  pnt3  20777  qabvle  20790  ostth2lem2  20799  ostth3  20803  ostth  20804  isgrp2d  20918  ghgrp  21051  ghablo  21052  smcnlem  21286  nmobndi  21369  ubthlem1  21465  ubthlem3  21467  htthlem  21513  pjhthlem2  21987  pjspansn  22172  5oalem6  22254  leopmuli  22729  pjnormssi  22764  pjclem4  22795  pj3si  22803  hatomistici  22958  sumdmdlem  23014  reximddv  23044  xmulcand  23120  suppss2f  23216  xrge0tsmsd  23397  subfacp1lem5  23730  erdszelem7  23743  erdszelem11  23747  cnpcon  23776  pconcon  23777  txpcon  23778  conpcon  23781  pconpi1  23783  sconpi1  23785  txscon  23787  cvxscon  23789  cnllyscon  23791  cvmsss2  23820  cvmcov2  23821  cvmopnlem  23824  cvmfolem  23825  cvmliftmolem2  23828  cvmliftlem7  23837  cvmliftlem10  23840  cvmliftlem15  23844  cvmlift2lem10  23858  cvmliftpht  23864  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3lem8  23872  umgraex  23890  eupai  23898  sinccvg  24021  dedekind  24097  dedekindle  24098  mulge0b  24101  prodmolem2  24158  zprod  24160  fprod  24164  fprodf1o  24172  nofulllem4  24430  colinearalglem4  24609  axcontlem10  24673  btwnouttr2  24717  cgrxfr  24750  btwnxfr  24751  brcolinear  24754  lineext  24771  btwnconn1lem13  24794  midofsegid  24799  segcon2  24800  brsegle  24803  seglecgr12im  24805  segletr  24809  colinbtwnle  24813  broutsideof2  24817  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  outsideofeq  24825  outsideofeu  24826  outsidele  24827  lineunray  24842  lineelsb2  24843  linethru  24848  supaddc  24995  ovoliunnfl  25001  itg2addnclem  25003  ftc1cnnc  25025  intopcoaconc  25644  efilcp  25655  iscnp4  25666  flfnei2  25680  icccon3  25804  finminlem  26334  nn0prpwlem  26341  locfincmp  26407  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  neibastop2  26413  neibastop3  26414  topjoin  26417  tailfb  26429  sdclem2  26555  fdc  26558  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  isbndx  26609  isbnd2  26610  isbnd3  26611  ssbnd  26615  totbndbnd  26616  prdsbnd  26620  prdsbnd2  26622  cntotbnd  26623  heibor1lem  26636  heibor1  26637  heiborlem9  26646  heiborlem10  26647  heibor  26648  rrncmslem  26659  ghomco  26676  1idl  26754  unichnidl  26759  prtlem10  26836  prtlem18  26848  elrfi  26872  isnacs3  26888  nacsfix  26890  fnwe2lem2  27251  kelac1  27264  lmhmfgsplit  27287  dsmmsubg  27312  dsmmlss  27313  frlmsslsp  27351  unxpwdom3  27359  enfixsn  27360  lindff1  27393  lindfrn  27394  hbtlem5  27435  hbt  27437  dgraa0p  27457  f1omvdco2  27494  psgnunilem1  27519  psgnunilem2  27521  psgnunilem3  27522  hashgcdeq  27620  rlimdmafv  28145  atlatmstc  30131  cvrexchlem  30230  paddasslem14  30644  pexmidlem5N  30785  cdleme29ex  31185  cdlemefr29exN  31213  cdleme32fva  31248  diarnN  31941  dihlsscpre  32046
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 177  df-an 360
  Copyright terms: Public domain W3C validator