MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expr Structured version   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  2823  disjxiun  4201  wereu2  4571  suppss  5855  fcof1  6012  knatar  6072  ovmpt2df  6197  suppss2  6292  riota5f  6566  smoord  6619  tfrlem9a  6639  oaass  6796  oelimcl  6835  oaabs2  6880  swoso  6928  eceqoveq  7001  domdifsn  7183  domunsncan  7200  omxpenlem  7201  mapdom2  7270  frfi  7344  fofinf1o  7379  finsschain  7405  elfiun  7427  marypha1lem  7430  eqsupd  7452  ordiso2  7474  ordtypelem6  7482  ordtypelem7  7483  ordtypelem10  7486  oismo  7499  wemapso2lem  7509  brwdom2  7531  wdomtr  7533  unwdomg  7542  xpwdomg  7543  unxpwdom2  7546  cantnfval2  7614  cantnfle  7616  cantnfreslem  7621  cantnflem1  7635  cantnf  7639  r1ordg  7694  tcrank  7798  carddomi2  7847  harval2  7874  infxpenlem  7885  infxpenc2lem2  7891  fseqenlem1  7895  dfac8clem  7903  acndom2  7925  infpwfien  7933  iunfictbso  7985  dfac12lem3  8015  infxp  8085  coflim  8131  cofsmo  8139  coftr  8143  sornom  8147  infpssrlem4  8176  enfin2i  8191  fin23lem26  8195  fin23lem27  8198  fin23lem36  8218  fin23lem40  8221  isf32lem5  8227  isf34lem4  8247  isfin1-3  8256  fin1a2lem10  8279  fin1a2lem13  8282  fin1a2s  8284  hsmexlem4  8299  ttukeylem5  8383  ttukeylem6  8384  ttukeylem7  8385  alephval2  8437  gchor  8492  fpwwe2lem7  8501  fpwwe2lem12  8506  fpwwe2  8508  pwfseqlem4a  8526  pwfseqlem4  8527  winalim2  8561  gchina  8564  inar1  8640  nqereq  8802  prlem934  8900  prlem936  8914  supsrlem  8976  axpre-sup  9034  prodge0  9847  supmul1  9963  un0addcl  10243  un0mulcl  10244  uzwo3  10559  qbtwnre  10775  xlemul1a  10857  seqcl2  11331  seqfveq2  11335  seqshft2  11339  monoord  11343  seqsplit  11346  seqf1olem1  11352  seqid2  11359  seqhomo  11360  expnegz  11404  expcan  11422  ltexp2  11423  discr  11506  bcval5  11599  hashbc  11692  hashf1lem2  11695  seqcoll  11702  seqcoll2  11703  wrdind  11781  cau3lem  12148  ello1d  12307  lo1bdd2  12308  rlimclim  12330  climrlim2  12331  rlimdm  12335  rlimcn1  12372  reccn2  12380  rlimsqzlem  12432  lo1le  12435  caucvgrlem  12456  caurcvg2  12461  summolem2  12500  zsum  12502  fsum  12504  fsumf1o  12507  sumss  12508  fsumss  12509  fsumcl2lem  12515  fsumadd  12522  fsumcom2  12548  fsum0diag2  12556  fsummulc2  12557  fsumconst  12563  fsumrelem  12576  fsumrlim  12580  fsumo1  12581  divrcnv  12622  geomulcvg  12643  mertenslem2  12652  ruclem8  12826  dvds0lem  12850  dvdsnegb  12857  dvdssub2  12877  bitsf1  12948  bitsshft  12977  bezoutlem3  13030  bezoutlem4  13031  isprm2lem  13076  isprm6  13099  isprm5  13102  pcqmul  13217  pcqcl  13220  pcxcl  13224  pc2dvds  13242  pcadd  13248  pcmpt  13251  pockthg  13264  infpnlem1  13268  prmreclem5  13278  vdwlem2  13340  vdwlem9  13347  vdwlem10  13348  vdwlem12  13350  ramub  13371  0ram  13378  ramub1lem2  13385  ramub1  13386  ramcl  13387  mreexexd  13863  acsfn2  13878  iscatd  13888  catpropd  13925  setcmon  14232  drsdirfi  14385  pleval2i  14411  psss  14636  mhmeql  14754  gsumvallem1  14761  frmdss2  14798  frmdup3  14801  grprcan  14828  mulgnn0ass  14909  isnsg3  14964  ghmpreima  15017  ghmeql  15018  gaorber  15075  oddvds  15175  gexdvds  15208  sylow1lem1  15222  odcau  15228  pgpssslw  15238  sylow2alem2  15242  sylow2blem3  15246  fislw  15249  sylow2  15250  lsmmod  15297  efgredlem  15369  frgpup3  15400  gexex  15458  gsumval3  15504  gsumzres  15507  gsumzcl  15508  gsumzf1o  15509  gsumzaddlem  15516  gsumconst  15522  gsumzmhm  15523  gsumzoppg  15529  gsum2d2lem  15537  ablfac1eulem  15620  pgpfac1lem5  15627  ablfaclem3  15635  issubdrg  15883  lss1d  16029  lmhmeql  16121  lspextmo  16122  lspsnat  16207  lsppratlem6  16214  islbs3  16217  lbsextlem4  16223  lidl1el  16279  mvrf1  16479  mplsubglem  16488  mpllsslem  16489  mplcoe1  16518  mplcoe2  16520  cnsubrg  16749  gsumfsum  16756  prmirredlem  16763  znidomb  16832  frgpcyg  16844  cssmre  16910  en2top  17040  toponmre  17147  topssnei  17178  innei  17179  clslp  17202  restcls  17235  restntr  17236  ordtrest2lem  17257  cnpco  17321  cncls2  17327  cncnpi  17332  cncnp  17334  cnconst2  17337  cnpdis  17347  lmcnp  17358  cnhaus  17408  nrmsep  17411  regsep2  17430  isreg2  17431  cncmp  17445  tgcmp  17454  sscmp  17458  cmpfi  17461  cnconn  17475  iunconlem  17480  clscon  17483  1stcfb  17498  1stcrest  17506  2ndcctbss  17508  2ndcdisj  17509  1stcelcls  17514  1stccnp  17515  restnlly  17535  cldllycmp  17548  lly1stc  17549  dislly  17550  kgentopon  17560  kgenidm  17569  1stckgenlem  17575  kgencn3  17580  ptpjpre1  17593  ptbasin  17599  txcls  17626  tx2cn  17632  ptpjcn  17633  ptclsg  17637  ptcnp  17644  txdis  17654  txlly  17658  txnlly  17659  pthaus  17660  txtube  17662  txcmplem1  17663  txcmplem2  17664  txcmp  17665  txhaus  17669  txkgen  17674  xkohaus  17675  xkococnlem  17681  xkococn  17682  txcon  17711  qtopeu  17738  qtoprest  17739  regr1lem2  17762  kqreglem1  17763  cmphaushmeo  17822  xkocnv  17836  fgabs  17901  filuni  17907  trufil  17932  ufileu  17941  filufint  17942  fin1aufil  17954  elfm2  17970  rnelfmlem  17974  fmfnfmlem2  17977  fmfnfmlem4  17979  fmufil  17981  flimopn  17997  fbflim2  17999  hausflimi  18002  hausflim  18003  flimcf  18004  flimclslem  18006  flimsncls  18008  hauspwpwf1  18009  cnpflfi  18021  fclsnei  18041  fclscf  18047  flimfnfcls  18050  fclscmp  18052  ufilcmp  18054  fcfnei  18057  cnpfcf  18063  alexsublem  18065  alexsub  18066  alexsubALTlem2  18069  alexsubALTlem3  18070  alexsubALTlem4  18071  ptcmplem3  18075  ptcmplem4  18076  ptcmplem5  18077  symgtgp  18121  tgpconcompeqg  18131  tgpconcomp  18132  ghmcnp  18134  tgpt0  18138  divstgplem  18140  haustsms2  18156  tsmsgsum  18158  tsmsres  18163  tsmsxp  18174  imasdsf1olem  18393  xbln0  18434  blssps  18444  blss  18445  neibl  18521  blcld  18525  metss  18528  metequiv2  18530  met1stc  18541  metrest  18544  prdsxmslem2  18549  metcnp3  18560  nrmmetd  18612  nlmvscnlem1  18712  nrginvrcnlem  18716  nmoleub  18755  icccmplem2  18844  icccmp  18846  reconnlem2  18848  xrge0tsms  18855  metdstri  18871  metdseq0  18874  metdscn  18876  cnmpt2pc  18943  cnheibor  18970  lebnumlem3  18978  pcoval2  19031  pcopt  19037  nmoleub2lem  19112  nmhmcn  19118  ipcnlem1  19189  cfilfcls  19217  cmetcaulem  19231  iscmet3lem2  19235  iscmet3  19236  equivcau  19243  caubl  19250  lmcau  19255  bcthlem2  19268  bcthlem3  19269  bcthlem4  19270  bcthlem5  19271  ivthlem2  19339  ivthlem3  19340  ovoliunlem2  19389  ovolicc2lem2  19404  ovolicc2lem3  19405  ovolicc2lem5  19407  ovolicc2  19408  ismbl2  19413  nulmbl  19420  nulmbl2  19421  unmbl  19422  shftmbl  19423  voliunlem3  19436  volsup  19440  ioombl1lem4  19445  ioombl1  19446  icombl  19448  ioombl  19449  uniioombl  19471  opnmbllem  19483  volivth  19489  vitali  19495  ismbf3d  19536  mbflimsup  19548  i1fadd  19577  itg1addlem4  19581  itg2le  19621  itg2seq  19624  itg2lea  19626  itg2splitlem  19630  itg2split  19631  itg2mono  19635  itg2gt0  19642  itg2cnlem2  19644  itgss  19693  itgfsum  19708  itgcn  19724  ellimc3  19756  limcco  19770  limciun  19771  dvnres  19807  dvnfre  19828  rolle  19864  c1liplem1  19870  dvivth  19884  dvne0  19885  lhop1lem  19887  lhop1  19888  lhop  19890  dvcnvrelem1  19891  dvfsumrlim  19905  dvfsum2  19908  ftc1a  19911  ftc1lem6  19915  itgsubst  19923  tdeglem4  19973  mdegaddle  19987  mdegvscale  19988  mdegmullem  19991  deg1tmle  20030  ply1divex  20049  dvdsq1p  20073  fta1g  20080  fta1b  20082  plyco0  20101  coeeulem  20133  dgrlem  20138  plyco  20150  coemullem  20158  dgreq0  20173  dgrco  20183  plydivex  20204  quotcan  20216  aannenlem1  20235  aalioulem2  20240  aalioulem3  20241  taylthlem1  20279  ulmbdd  20304  ulmdvlem3  20308  itgulm  20314  radcnvlt1  20324  psercnlem1  20331  abelthlem2  20338  abelthlem8  20345  logcnlem5  20527  efopn  20539  cxpmul2z  20572  cxpcn3lem  20621  cxpeq  20631  xrlimcnp  20797  cxplim  20800  o1cxp  20803  cxploglim  20806  scvxcvx  20814  jensen  20817  ftalem1  20845  ftalem2  20846  fta  20852  basellem3  20855  isppw2  20888  ppinprm  20925  chtnprm  20927  dvdsmulf1o  20969  chtublem  20985  perfectlem2  21004  dchrfi  21029  dchrptlem1  21038  dchrptlem2  21039  dchrptlem3  21040  dchrsum2  21042  bposlem1  21058  bposlem3  21060  2sqlem5  21142  2sqlem6  21143  2sqlem8  21146  2sqlem10  21148  2sqb  21152  chebbnd1lem1  21153  chtppilimlem2  21158  dchrisum0flb  21194  dchrisum0fno1  21195  dchrisum0  21204  pntrsumbnd2  21251  pntpbnd1  21270  pntpbnd2  21271  pntlemp  21294  pnt3  21296  qabvle  21309  ostth2lem2  21318  ostth3  21322  ostth  21323  umgraex  21348  eupai  21679  isgrp2d  21813  ghgrp  21946  ghablo  21947  smcnlem  22183  ubthlem1  22362  ubthlem3  22364  htthlem  22410  pjhthlem2  22884  5oalem6  23151  leopmuli  23626  pjnormssi  23661  pjclem4  23692  pj3si  23700  hatomistici  23855  sumdmdlem  23911  reximddv  23952  suppss2f  24039  xrge0tsmsd  24213  qqhf  24360  ballotlemfc0  24740  ballotlemfcc  24741  subfacp1lem5  24860  erdszelem7  24873  erdszelem11  24877  pconcon  24908  txpcon  24909  conpcon  24912  sconpi1  24916  txscon  24918  cvxscon  24920  cvmopnlem  24955  cvmfolem  24956  cvmliftmolem2  24959  cvmliftlem7  24968  cvmliftlem10  24971  cvmliftlem15  24975  cvmlift2lem10  24989  cvmlift3lem4  24999  cvmlift3lem8  25003  dedekind  25177  dedekindle  25178  mulge0b  25181  prodmolem2  25251  zprod  25253  fprod  25257  fprodf1o  25262  prodss  25263  fprodss  25264  fprodcl2lem  25266  fprodmul  25274  fproddiv  25275  fprodconst  25292  fprodn0  25293  fprodcom2  25298  nofulllem4  25625  colinearalglem4  25813  axcontlem10  25877  btwnouttr2  25921  cgrxfr  25954  btwnxfr  25955  brcolinear  25958  lineext  25975  btwnconn1lem13  25998  midofsegid  26003  segcon2  26004  brsegle  26007  seglecgr12im  26009  segletr  26013  colinbtwnle  26017  broutsideof2  26021  btwnoutside  26024  broutsideof3  26025  outsideoftr  26028  outsideofeq  26029  outsideofeu  26030  outsidele  26031  lineunray  26046  lineelsb2  26047  linethru  26052  supaddc  26201  mblfinlem  26207  mblfinlem2  26208  ismblfin  26210  ovoliunnfl  26211  voliunnfl  26213  volsupnfl  26214  itg2addnclem  26219  itg2addnclem3  26221  ftc1cnnc  26242  finminlem  26275  nn0prpwlem  26279  locfincmp  26338  comppfsc  26341  neibastop2lem  26343  neibastop2  26344  neibastop3  26345  topjoin  26348  tailfb  26360  sdclem2  26400  fdc  26403  istotbnd3  26434  isbnd2  26446  isbnd3  26447  prdsbnd  26456  cntotbnd  26459  heibor1lem  26472  heibor1  26473  heiborlem10  26483  rrncmslem  26495  ghomco  26512  1idl  26590  unichnidl  26595  prtlem10  26668  prtlem18  26680  isnacs3  26718  nacsfix  26720  fnwe2lem2  27080  kelac1  27093  dsmmsubg  27141  dsmmlss  27142  frlmsslsp  27180  unxpwdom3  27188  enfixsn  27189  lindff1  27222  lindfrn  27223  hbtlem5  27264  hbt  27266  dgraa0p  27286  f1omvdco2  27323  psgnunilem1  27348  psgnunilem2  27350  hashgcdeq  27449  rlimdmafv  27972  modprminv  28155  modprminveq  28156  reumodprminv  28157  cshwidx  28172  atlatmstc  30018  cvrexchlem  30117  paddasslem14  30531  pexmidlem5N  30672  cdleme29ex  31072  cdlemefr29exN  31100  cdleme32fva  31135  diarnN  31828  dihlsscpre  31933
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