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

Theorem expr 610
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 600 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 429 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  reximddv  2819  rexlimdvaa  2832  disjxiun  4277  wereu2  4704  suppssOLD  5824  fcof1  5978  knatar  6035  riota5f  6065  ovmpt2df  6211  suppss2OLD  6304  extmptsuppeq  6702  suppss  6708  suppss2  6712  smoord  6812  tfrlem9a  6831  oaass  6988  oelimcl  7027  oaabs2  7072  swoso  7120  eceqoveq  7193  domdifsn  7382  domunsncan  7399  omxpenlem  7400  enfixsn  7408  mapdom2  7470  frfi  7545  fofinf1o  7580  finsschain  7606  elfiun  7668  marypha1lem  7671  eqsupd  7695  ordiso2  7717  ordtypelem6  7725  ordtypelem7  7726  ordtypelem10  7729  oismo  7742  wemapsolem  7752  brwdom2  7776  wdomtr  7778  unwdomg  7787  xpwdomg  7788  unxpwdom2  7791  cantnfval2  7865  cantnfle  7867  cantnflem1  7885  cantnf  7889  cantnfval2OLD  7895  cantnfleOLD  7897  cantnflem1OLD  7908  cantnfOLD  7911  r1ordg  7973  tcrank  8079  carddomi2  8128  harval2  8155  infxpenlem  8168  infxpenc2lem2  8174  infxpenc2lem2OLD  8178  fseqenlem1  8182  dfac8clem  8190  acndom2  8212  infpwfien  8220  iunfictbso  8272  dfac12lem3  8302  infxp  8372  coflim  8418  cofsmo  8426  coftr  8430  sornom  8434  infpssrlem4  8463  enfin2i  8478  fin23lem26  8482  fin23lem27  8485  fin23lem36  8505  fin23lem40  8508  isf32lem5  8514  isf34lem4  8534  isfin1-3  8543  fin1a2lem10  8566  fin1a2lem13  8569  fin1a2s  8571  hsmexlem4  8586  ttukeylem5  8670  ttukeylem6  8671  ttukeylem7  8672  alephval2  8724  gchor  8782  fpwwe2lem7  8791  fpwwe2lem12  8796  fpwwe2  8798  pwfseqlem4a  8816  pwfseqlem4  8817  winalim2  8851  gchina  8854  inar1  8930  nqereq  9092  prlem934  9190  prlem936  9204  supsrlem  9266  axpre-sup  9324  dedekind  9521  dedekindle  9522  prodge0  10164  mulge0b  10187  supmul1  10283  un0addcl  10601  un0mulcl  10602  uzwo3  10936  qbtwnre  11157  xlemul1a  11239  seqcl2  11808  seqfveq2  11812  seqshft2  11816  monoord  11820  seqsplit  11823  seqf1olem1  11829  seqid2  11836  seqhomo  11837  expnegz  11882  expcan  11900  ltexp2  11901  discr  11985  bcval5  12078  hashbc  12190  hashf1lem2  12193  seqcoll  12200  seqcoll2  12201  wrdind  12355  wrd2ind  12356  cau3lem  12826  ello1d  12985  lo1bdd2  12986  rlimclim  13008  climrlim2  13009  rlimdm  13013  rlimcn1  13050  reccn2  13058  rlimsqzlem  13110  lo1le  13113  caucvgrlem  13134  caurcvg2  13139  summolem2  13177  zsum  13179  fsum  13181  fsumf1o  13184  sumss  13185  fsumss  13186  fsumcl2lem  13192  fsumadd  13199  fsumcom2  13225  fsum0diag2  13233  fsummulc2  13234  fsumconst  13240  fsumrelem  13253  fsumrlim  13257  fsumo1  13258  divrcnv  13298  geomulcvg  13319  mertenslem2  13328  ruclem8  13502  dvds0lem  13526  dvdsnegb  13533  dvdssub2  13553  bitsf1  13625  bitsshft  13654  bezoutlem3  13707  bezoutlem4  13708  isprm2lem  13753  isprm6  13778  isprm5  13781  modprminv  13853  modprminveq  13854  reumodprminv  13855  pcqmul  13903  pcqcl  13906  pcxcl  13910  pc2dvds  13928  pcadd  13934  pcmpt  13937  pockthg  13950  infpnlem1  13954  prmreclem5  13964  vdwlem2  14026  vdwlem9  14033  vdwlem10  14034  vdwlem12  14036  ramub  14057  0ram  14064  ramub1lem2  14071  ramub1  14072  ramcl  14073  mreexexd  14569  acsfn2  14584  iscatd  14594  catpropd  14631  setcmon  14938  drsdirfi  15091  pleval2i  15117  psss  15367  mhmeql  15474  gsumvallem1  15482  frmdss2  15521  frmdup3  15524  grprcan  15551  mulgnn0ass  15636  isnsg3  15695  ghmpreima  15748  ghmeql  15749  gaorber  15806  f1omvdco2  15934  psgnunilem1  15979  psgnunilem2  15981  oddvds  16030  gexdvds  16063  sylow1lem1  16077  odcau  16083  pgpssslw  16093  sylow2alem2  16097  sylow2blem3  16101  fislw  16104  sylow2  16105  lsmmod  16152  efgredlem  16224  frgpup3  16255  gexex  16315  gsumval3OLD  16362  gsumval3  16365  gsumzres  16368  gsumzcl2  16369  gsumzf1o  16371  gsumzresOLD  16372  gsumzclOLD  16373  gsumzf1oOLD  16374  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  gsumzoppg  16416  gsumzoppgOLD  16417  gsum2d2lem  16439  ablfac1eulem  16547  pgpfac1lem5  16554  ablfaclem3  16562  issubdrg  16814  lss1d  16966  lmhmeql  17058  lspextmo  17059  lspsnat  17148  lsppratlem6  17155  islbs3  17158  lbsextlem4  17164  lidl1el  17222  mvrf1  17432  mplsubglem  17444  mpllsslem  17445  mplsubglemOLD  17446  mpllsslemOLD  17447  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  cnsubrg  17717  gsumfsum  17723  prmirredlem  17759  prmirredlemOLD  17762  znidomb  17836  frgpcyg  17848  cssmre  17960  dsmmsubg  18010  dsmmlss  18011  frlmsslsp  18065  frlmsslspOLD  18066  lindff1  18091  lindfrn  18092  mdet1  18250  mdetunilem7  18266  mdetunilem8  18267  mdetunilem9  18268  en2top  18432  toponmre  18539  topssnei  18570  innei  18571  clslp  18594  restcls  18627  restntr  18628  ordtrest2lem  18649  cnpco  18713  cncls2  18719  cncnpi  18724  cncnp  18726  cnconst2  18729  cnpdis  18739  lmcnp  18750  cnhaus  18800  nrmsep  18803  regsep2  18822  isreg2  18823  cncmp  18837  tgcmp  18846  sscmp  18850  cmpfi  18853  cnconn  18868  iunconlem  18873  clscon  18876  1stcfb  18891  1stcrest  18899  2ndcctbss  18901  2ndcdisj  18902  1stcelcls  18907  1stccnp  18908  restnlly  18928  cldllycmp  18941  lly1stc  18942  dislly  18943  kgentopon  18953  kgenidm  18962  1stckgenlem  18968  kgencn3  18973  ptpjpre1  18986  ptbasin  18992  txcls  19019  tx2cn  19025  ptpjcn  19026  ptclsg  19030  ptcnp  19037  txdis  19047  txlly  19051  txnlly  19052  pthaus  19053  txtube  19055  txcmplem1  19056  txcmplem2  19057  txcmp  19058  txhaus  19062  txkgen  19067  xkohaus  19068  xkococnlem  19074  xkococn  19075  txcon  19104  qtopeu  19131  qtoprest  19132  regr1lem2  19155  kqreglem1  19156  cmphaushmeo  19215  xkocnv  19229  fgabs  19294  filuni  19300  trufil  19325  ufileu  19334  filufint  19335  fin1aufil  19347  elfm2  19363  rnelfmlem  19367  fmfnfmlem2  19370  fmfnfmlem4  19372  fmufil  19374  flimopn  19390  fbflim2  19392  hausflimi  19395  hausflim  19396  flimcf  19397  flimclslem  19399  flimsncls  19401  hauspwpwf1  19402  cnpflfi  19414  fclsnei  19434  fclscf  19440  flimfnfcls  19443  fclscmp  19445  ufilcmp  19447  fcfnei  19450  cnpfcf  19456  alexsublem  19458  alexsub  19459  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  ptcmplem3  19468  ptcmplem4  19469  ptcmplem5  19470  symgtgp  19514  tgpconcompeqg  19524  tgpconcomp  19525  ghmcnp  19527  tgpt0  19531  divstgplem  19533  haustsms2  19549  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  tsmsxp  19571  imasdsf1olem  19790  xbln0  19831  blssps  19841  blss  19842  neibl  19918  blcld  19922  metss  19925  metequiv2  19927  met1stc  19938  metrest  19941  prdsxmslem2  19946  metcnp3  19957  nrmmetd  20009  nlmvscnlem1  20109  nrginvrcnlem  20113  nmoleub  20152  icccmplem2  20242  icccmp  20244  reconnlem2  20246  xrge0tsms  20253  metdstri  20269  metdseq0  20272  metdscn  20274  cnmpt2pc  20342  cnheibor  20369  lebnumlem3  20377  pcoval2  20430  pcopt  20436  nmoleub2lem  20511  nmhmcn  20517  ipcnlem1  20599  cfilfcls  20627  cmetcaulem  20641  iscmet3lem2  20645  iscmet3  20646  equivcau  20653  caubl  20660  lmcau  20665  bcthlem2  20678  bcthlem3  20679  bcthlem4  20680  bcthlem5  20681  ivthlem2  20778  ivthlem3  20779  ovoliunlem2  20828  ovolicc2lem2  20843  ovolicc2lem3  20844  ovolicc2lem5  20846  ovolicc2  20847  ismbl2  20852  nulmbl  20859  nulmbl2  20860  unmbl  20861  shftmbl  20862  voliunlem3  20875  volsup  20879  ioombl1lem4  20884  ioombl1  20885  icombl  20887  ioombl  20888  uniioombl  20911  opnmbllem  20923  volivth  20929  vitali  20935  ismbf3d  20974  mbflimsup  20986  i1fadd  21015  itg1addlem4  21019  itg2le  21059  itg2seq  21062  itg2lea  21064  itg2splitlem  21068  itg2split  21069  itg2mono  21073  itg2gt0  21080  itg2cnlem2  21082  itgss  21131  itgfsum  21146  itgcn  21162  ellimc3  21196  limcco  21210  limciun  21211  dvnres  21247  dvnfre  21268  rolle  21304  c1liplem1  21310  dvivth  21324  dvne0  21325  lhop1lem  21327  lhop1  21328  lhop  21330  dvcnvrelem1  21331  dvfsumrlim  21345  dvfsum2  21348  ftc1a  21351  ftc1lem6  21355  itgsubst  21363  tdeglem4  21414  mdegaddle  21430  mdegvscale  21431  mdegmullem  21434  deg1tmle  21474  ply1divex  21493  dvdsq1p  21517  fta1g  21524  fta1b  21526  plyco0  21545  coeeulem  21577  dgrlem  21582  plyco  21594  coemullem  21602  dgreq0  21617  dgrco  21627  plydivex  21648  quotcan  21660  aannenlem1  21679  aalioulem2  21684  aalioulem3  21685  taylthlem1  21723  ulmbdd  21748  ulmdvlem3  21752  itgulm  21758  radcnvlt1  21768  psercnlem1  21775  abelthlem2  21782  abelthlem8  21789  logcnlem5  21976  efopn  21988  cxpmul2z  22021  cxpcn3lem  22070  cxpeq  22080  xrlimcnp  22247  cxplim  22250  o1cxp  22253  cxploglim  22256  scvxcvx  22264  jensen  22267  ftalem1  22295  ftalem2  22296  fta  22302  basellem3  22305  isppw2  22338  ppinprm  22375  chtnprm  22377  dvdsmulf1o  22419  chtublem  22435  perfectlem2  22454  dchrfi  22479  dchrptlem1  22488  dchrptlem2  22489  dchrptlem3  22490  dchrsum2  22492  bposlem1  22508  bposlem3  22510  2sqlem5  22592  2sqlem6  22593  2sqlem8  22596  2sqlem10  22598  2sqb  22602  chebbnd1lem1  22603  chtppilimlem2  22608  dchrisum0flb  22644  dchrisum0fno1  22645  dchrisum0  22654  pntrsumbnd2  22701  pntpbnd1  22720  pntpbnd2  22721  pntlemp  22744  pnt3  22746  qabvle  22759  ostth2lem2  22768  ostth3  22772  ostth  22773  colinearalglem4  22978  axcontlem10  23042  umgraex  23080  eupai  23411  isgrp2d  23545  ghgrp  23678  ghablo  23679  smcnlem  23915  ubthlem1  24094  ubthlem3  24096  htthlem  24142  pjhthlem2  24618  5oalem6  24885  leopmuli  25360  pjnormssi  25395  pjclem4  25426  pj3si  25434  hatomistici  25589  sumdmdlem  25645  suppss2f  25778  xrge0tsmsd  26106  isarchiofld  26138  ordtrest2NEWlem  26206  qqhf  26269  eulerpartlemb  26599  ballotlemfc0  26723  ballotlemfcc  26724  sgn3da  26772  subfacp1lem5  26920  erdszelem7  26933  erdszelem11  26937  pconcon  26968  txpcon  26969  conpcon  26972  sconpi1  26976  txscon  26978  cvxscon  26980  cvmopnlem  27015  cvmfolem  27016  cvmliftmolem2  27019  cvmliftlem7  27028  cvmliftlem10  27031  cvmliftlem15  27035  cvmlift2lem10  27049  cvmlift3lem4  27059  cvmlift3lem8  27063  prodmolem2  27295  zprod  27297  fprod  27301  fprodf1o  27306  prodss  27307  fprodss  27308  fprodcl2lem  27310  fprodmul  27318  fproddiv  27319  fprodconst  27336  fprodn0  27337  fprodcom2  27342  wzel  27608  wsuclem  27609  nofulllem4  27693  btwnouttr2  27900  cgrxfr  27933  btwnxfr  27934  brcolinear  27937  lineext  27954  btwnconn1lem13  27977  midofsegid  27982  segcon2  27983  brsegle  27986  seglecgr12im  27988  segletr  27992  colinbtwnle  27996  broutsideof2  28000  btwnoutside  28003  broutsideof3  28004  outsideoftr  28007  outsideofeq  28008  outsideofeu  28009  outsidele  28010  lineunray  28025  lineelsb2  28026  linethru  28031  wl-sbcom2d-lem1  28233  finixpnum  28258  supaddc  28261  heicant  28270  opnmbllem0  28271  mblfinlem3  28274  ismblfin  28276  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  itg2addnclem  28287  itg2addnclem3  28289  ftc1cnnc  28310  finminlem  28357  nn0prpwlem  28361  locfincmp  28420  comppfsc  28423  neibastop2lem  28425  neibastop2  28426  neibastop3  28427  topjoin  28430  tailfb  28442  sdclem2  28482  fdc  28485  istotbnd3  28514  isbnd2  28526  isbnd3  28527  prdsbnd  28536  cntotbnd  28539  heibor1lem  28552  heibor1  28553  heiborlem10  28563  rrncmslem  28575  ghomco  28592  1idl  28670  unichnidl  28675  prtlem10  28855  prtlem18  28867  isnacs3  28891  nacsfix  28893  fnwe2lem2  29249  kelac1  29261  unxpwdom3  29293  hbtlem5  29329  hbt  29331  dgraa0p  29351  hashgcdeq  29411  rlimdmafv  29929  numclwwlkovf2ex  30525  lindslinindsimp2  30706  atlatmstc  32537  cvrexchlem  32636  paddasslem14  33050  pexmidlem5N  33191  cdleme29ex  33591  cdlemefr29exN  33619  cdleme32fva  33654  diarnN  34347  dihlsscpre  34452
  Copyright terms: Public domain W3C validator