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

Theorem expr 615
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 605 . 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  2824  rexlimdvaa  2837  disjxiun  4284  wereu2  4712  suppssOLD  5831  fcof1  5986  knatar  6043  riota5f  6072  ovmpt2df  6217  suppss2OLD  6310  extmptsuppeq  6708  suppss  6714  suppss2  6718  smoord  6818  tfrlem9a  6837  oaass  6992  oelimcl  7031  oaabs2  7076  swoso  7124  eceqoveq  7197  domdifsn  7386  domunsncan  7403  omxpenlem  7404  enfixsn  7412  mapdom2  7474  frfi  7549  fofinf1o  7584  finsschain  7610  elfiun  7672  marypha1lem  7675  eqsupd  7699  ordiso2  7721  ordtypelem6  7729  ordtypelem7  7730  ordtypelem10  7733  oismo  7746  wemapsolem  7756  brwdom2  7780  wdomtr  7782  unwdomg  7791  xpwdomg  7792  unxpwdom2  7795  cantnfval2  7869  cantnfle  7871  cantnflem1  7889  cantnf  7893  cantnfval2OLD  7899  cantnfleOLD  7901  cantnflem1OLD  7912  cantnfOLD  7915  r1ordg  7977  tcrank  8083  carddomi2  8132  harval2  8159  infxpenlem  8172  infxpenc2lem2  8178  infxpenc2lem2OLD  8182  fseqenlem1  8186  dfac8clem  8194  acndom2  8216  infpwfien  8224  iunfictbso  8276  dfac12lem3  8306  infxp  8376  coflim  8422  cofsmo  8430  coftr  8434  sornom  8438  infpssrlem4  8467  enfin2i  8482  fin23lem26  8486  fin23lem27  8489  fin23lem36  8509  fin23lem40  8512  isf32lem5  8518  isf34lem4  8538  isfin1-3  8547  fin1a2lem10  8570  fin1a2lem13  8573  fin1a2s  8575  hsmexlem4  8590  ttukeylem5  8674  ttukeylem6  8675  ttukeylem7  8676  alephval2  8728  gchor  8786  fpwwe2lem7  8795  fpwwe2lem12  8800  fpwwe2  8802  pwfseqlem4a  8820  pwfseqlem4  8821  winalim2  8855  gchina  8858  inar1  8934  nqereq  9096  prlem934  9194  prlem936  9208  supsrlem  9270  axpre-sup  9328  dedekind  9525  dedekindle  9526  prodge0  10168  mulge0b  10191  supmul1  10287  un0addcl  10605  un0mulcl  10606  uzwo3  10940  qbtwnre  11161  xlemul1a  11243  seqcl2  11816  seqfveq2  11820  seqshft2  11824  monoord  11828  seqsplit  11831  seqf1olem1  11837  seqid2  11844  seqhomo  11845  expnegz  11890  expcan  11908  ltexp2  11909  discr  11993  bcval5  12086  hashbc  12198  hashf1lem2  12201  seqcoll  12208  seqcoll2  12209  wrdind  12363  wrd2ind  12364  cau3lem  12834  ello1d  12993  lo1bdd2  12994  rlimclim  13016  climrlim2  13017  rlimdm  13021  rlimcn1  13058  reccn2  13066  rlimsqzlem  13118  lo1le  13121  caucvgrlem  13142  caurcvg2  13147  summolem2  13185  zsum  13187  fsum  13189  fsumf1o  13192  sumss  13193  fsumss  13194  fsumcl2lem  13200  fsumadd  13207  fsumcom2  13233  fsum0diag2  13242  fsummulc2  13243  fsumconst  13249  fsumrelem  13262  fsumrlim  13266  fsumo1  13267  divrcnv  13307  geomulcvg  13328  mertenslem2  13337  ruclem8  13511  dvds0lem  13535  dvdsnegb  13542  dvdssub2  13562  bitsf1  13634  bitsshft  13663  bezoutlem3  13716  bezoutlem4  13717  isprm2lem  13762  isprm6  13787  isprm5  13790  modprminv  13862  modprminveq  13863  reumodprminv  13864  pcqmul  13912  pcqcl  13915  pcxcl  13919  pc2dvds  13937  pcadd  13943  pcmpt  13946  pockthg  13959  infpnlem1  13963  prmreclem5  13973  vdwlem2  14035  vdwlem9  14042  vdwlem10  14043  vdwlem12  14045  ramub  14066  0ram  14073  ramub1lem2  14080  ramub1  14081  ramcl  14082  mreexexd  14578  acsfn2  14593  iscatd  14603  catpropd  14640  setcmon  14947  drsdirfi  15100  pleval2i  15126  psss  15376  mhmeql  15483  gsumvallem1  15491  frmdss2  15532  frmdup3  15535  grprcan  15562  mulgnn0ass  15647  isnsg3  15706  ghmpreima  15759  ghmeql  15760  gaorber  15817  f1omvdco2  15945  psgnunilem1  15990  psgnunilem2  15992  oddvds  16041  gexdvds  16074  sylow1lem1  16088  odcau  16094  pgpssslw  16104  sylow2alem2  16108  sylow2blem3  16112  fislw  16115  sylow2  16116  lsmmod  16163  efgredlem  16235  frgpup3  16266  gexex  16326  gsumval3OLD  16373  gsumval3  16376  gsumzres  16379  gsumzcl2  16380  gsumzf1o  16382  gsumzresOLD  16383  gsumzclOLD  16384  gsumzf1oOLD  16385  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzoppg  16430  gsumzoppgOLD  16431  gsum2d2lem  16453  ablfac1eulem  16561  pgpfac1lem5  16568  ablfaclem3  16576  issubdrg  16868  lss1d  17021  lmhmeql  17113  lspextmo  17114  lspsnat  17203  lsppratlem6  17210  islbs3  17213  lbsextlem4  17219  lidl1el  17277  mvrf1  17475  mplsubglem  17487  mpllsslem  17488  mplsubglemOLD  17489  mpllsslemOLD  17490  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  cnsubrg  17848  gsumfsum  17854  prmirredlem  17892  prmirredlemOLD  17895  znidomb  17969  frgpcyg  17981  cssmre  18093  dsmmsubg  18143  dsmmlss  18144  frlmsslsp  18198  frlmsslspOLD  18199  lindff1  18224  lindfrn  18225  mdet1  18383  mdetunilem7  18399  mdetunilem8  18400  mdetunilem9  18401  en2top  18565  toponmre  18672  topssnei  18703  innei  18704  clslp  18727  restcls  18760  restntr  18761  ordtrest2lem  18782  cnpco  18846  cncls2  18852  cncnpi  18857  cncnp  18859  cnconst2  18862  cnpdis  18872  lmcnp  18883  cnhaus  18933  nrmsep  18936  regsep2  18955  isreg2  18956  cncmp  18970  tgcmp  18979  sscmp  18983  cmpfi  18986  cnconn  19001  iunconlem  19006  clscon  19009  1stcfb  19024  1stcrest  19032  2ndcctbss  19034  2ndcdisj  19035  1stcelcls  19040  1stccnp  19041  restnlly  19061  cldllycmp  19074  lly1stc  19075  dislly  19076  kgentopon  19086  kgenidm  19095  1stckgenlem  19101  kgencn3  19106  ptpjpre1  19119  ptbasin  19125  txcls  19152  tx2cn  19158  ptpjcn  19159  ptclsg  19163  ptcnp  19170  txdis  19180  txlly  19184  txnlly  19185  pthaus  19186  txtube  19188  txcmplem1  19189  txcmplem2  19190  txcmp  19191  txhaus  19195  txkgen  19200  xkohaus  19201  xkococnlem  19207  xkococn  19208  txcon  19237  qtopeu  19264  qtoprest  19265  regr1lem2  19288  kqreglem1  19289  cmphaushmeo  19348  xkocnv  19362  fgabs  19427  filuni  19433  trufil  19458  ufileu  19467  filufint  19468  fin1aufil  19480  elfm2  19496  rnelfmlem  19500  fmfnfmlem2  19503  fmfnfmlem4  19505  fmufil  19507  flimopn  19523  fbflim2  19525  hausflimi  19528  hausflim  19529  flimcf  19530  flimclslem  19532  flimsncls  19534  hauspwpwf1  19535  cnpflfi  19547  fclsnei  19567  fclscf  19573  flimfnfcls  19576  fclscmp  19578  ufilcmp  19580  fcfnei  19583  cnpfcf  19589  alexsublem  19591  alexsub  19592  alexsubALTlem2  19595  alexsubALTlem3  19596  alexsubALTlem4  19597  ptcmplem3  19601  ptcmplem4  19602  ptcmplem5  19603  symgtgp  19647  tgpconcompeqg  19657  tgpconcomp  19658  ghmcnp  19660  tgpt0  19664  divstgplem  19666  haustsms2  19682  tsmsgsum  19684  tsmsgsumOLD  19687  tsmsresOLD  19692  tsmsres  19693  tsmsxp  19704  imasdsf1olem  19923  xbln0  19964  blssps  19974  blss  19975  neibl  20051  blcld  20055  metss  20058  metequiv2  20060  met1stc  20071  metrest  20074  prdsxmslem2  20079  metcnp3  20090  nrmmetd  20142  nlmvscnlem1  20242  nrginvrcnlem  20246  nmoleub  20285  icccmplem2  20375  icccmp  20377  reconnlem2  20379  xrge0tsms  20386  metdstri  20402  metdseq0  20405  metdscn  20407  cnmpt2pc  20475  cnheibor  20502  lebnumlem3  20510  pcoval2  20563  pcopt  20569  nmoleub2lem  20644  nmhmcn  20650  ipcnlem1  20732  cfilfcls  20760  cmetcaulem  20774  iscmet3lem2  20778  iscmet3  20779  equivcau  20786  caubl  20793  lmcau  20798  bcthlem2  20811  bcthlem3  20812  bcthlem4  20813  bcthlem5  20814  ivthlem2  20911  ivthlem3  20912  ovoliunlem2  20961  ovolicc2lem2  20976  ovolicc2lem3  20977  ovolicc2lem5  20979  ovolicc2  20980  ismbl2  20985  nulmbl  20992  nulmbl2  20993  unmbl  20994  shftmbl  20995  voliunlem3  21008  volsup  21012  ioombl1lem4  21017  ioombl1  21018  icombl  21020  ioombl  21021  uniioombl  21044  opnmbllem  21056  volivth  21062  vitali  21068  ismbf3d  21107  mbflimsup  21119  i1fadd  21148  itg1addlem4  21152  itg2le  21192  itg2seq  21195  itg2lea  21197  itg2splitlem  21201  itg2split  21202  itg2mono  21206  itg2gt0  21213  itg2cnlem2  21215  itgss  21264  itgfsum  21279  itgcn  21295  ellimc3  21329  limcco  21343  limciun  21344  dvnres  21380  dvnfre  21401  rolle  21437  c1liplem1  21443  dvivth  21457  dvne0  21458  lhop1lem  21460  lhop1  21461  lhop  21463  dvcnvrelem1  21464  dvfsumrlim  21478  dvfsum2  21481  ftc1a  21484  ftc1lem6  21488  itgsubst  21496  tdeglem4  21504  mdegaddle  21520  mdegvscale  21521  mdegmullem  21524  deg1tmle  21564  ply1divex  21583  dvdsq1p  21607  fta1g  21614  fta1b  21616  plyco0  21635  coeeulem  21667  dgrlem  21672  plyco  21684  coemullem  21692  dgreq0  21707  dgrco  21717  plydivex  21738  quotcan  21750  aannenlem1  21769  aalioulem2  21774  aalioulem3  21775  taylthlem1  21813  ulmbdd  21838  ulmdvlem3  21842  itgulm  21848  radcnvlt1  21858  psercnlem1  21865  abelthlem2  21872  abelthlem8  21879  logcnlem5  22066  efopn  22078  cxpmul2z  22111  cxpcn3lem  22160  cxpeq  22170  xrlimcnp  22337  cxplim  22340  o1cxp  22343  cxploglim  22346  scvxcvx  22354  jensen  22357  ftalem1  22385  ftalem2  22386  fta  22392  basellem3  22395  isppw2  22428  ppinprm  22465  chtnprm  22467  dvdsmulf1o  22509  chtublem  22525  perfectlem2  22544  dchrfi  22569  dchrptlem1  22578  dchrptlem2  22579  dchrptlem3  22580  dchrsum2  22582  bposlem1  22598  bposlem3  22600  2sqlem5  22682  2sqlem6  22683  2sqlem8  22686  2sqlem10  22688  2sqb  22692  chebbnd1lem1  22693  chtppilimlem2  22698  dchrisum0flb  22734  dchrisum0fno1  22735  dchrisum0  22744  pntrsumbnd2  22791  pntpbnd1  22810  pntpbnd2  22811  pntlemp  22834  pnt3  22836  qabvle  22849  ostth2lem2  22858  ostth3  22862  ostth  22863  colinearalglem4  23106  axcontlem10  23170  umgraex  23208  eupai  23539  isgrp2d  23673  ghgrp  23806  ghablo  23807  smcnlem  24043  ubthlem1  24222  ubthlem3  24224  htthlem  24270  pjhthlem2  24746  5oalem6  25013  leopmuli  25488  pjnormssi  25523  pjclem4  25554  pj3si  25562  hatomistici  25717  sumdmdlem  25773  suppss2f  25905  xrge0tsmsd  26204  isarchiofld  26236  ordtrest2NEWlem  26304  qqhf  26367  eulerpartlemb  26703  ballotlemfc0  26827  ballotlemfcc  26828  sgn3da  26876  subfacp1lem5  27024  erdszelem7  27037  erdszelem11  27041  pconcon  27072  txpcon  27073  conpcon  27076  sconpi1  27080  txscon  27082  cvxscon  27084  cvmopnlem  27119  cvmfolem  27120  cvmliftmolem2  27123  cvmliftlem7  27132  cvmliftlem10  27135  cvmliftlem15  27139  cvmlift2lem10  27153  cvmlift3lem4  27163  cvmlift3lem8  27167  prodmolem2  27399  zprod  27401  fprod  27405  fprodf1o  27410  prodss  27411  fprodss  27412  fprodcl2lem  27414  fprodmul  27422  fproddiv  27423  fprodconst  27440  fprodn0  27441  fprodcom2  27446  wzel  27712  wsuclem  27713  nofulllem4  27797  btwnouttr2  28004  cgrxfr  28037  btwnxfr  28038  brcolinear  28041  lineext  28058  btwnconn1lem13  28081  midofsegid  28086  segcon2  28087  brsegle  28090  seglecgr12im  28092  segletr  28096  colinbtwnle  28100  broutsideof2  28104  btwnoutside  28107  broutsideof3  28108  outsideoftr  28111  outsideofeq  28112  outsideofeu  28113  outsidele  28114  lineunray  28129  lineelsb2  28130  linethru  28135  wl-sbcom2d-lem1  28336  finixpnum  28367  supaddc  28370  heicant  28379  opnmbllem0  28380  mblfinlem3  28383  ismblfin  28385  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  itg2addnclem  28396  itg2addnclem3  28398  ftc1cnnc  28419  finminlem  28466  nn0prpwlem  28470  locfincmp  28529  comppfsc  28532  neibastop2lem  28534  neibastop2  28535  neibastop3  28536  topjoin  28539  tailfb  28551  sdclem2  28591  fdc  28594  istotbnd3  28623  isbnd2  28635  isbnd3  28636  prdsbnd  28645  cntotbnd  28648  heibor1lem  28661  heibor1  28662  heiborlem10  28672  rrncmslem  28684  ghomco  28701  1idl  28779  unichnidl  28784  prtlem10  28963  prtlem18  28975  isnacs3  28999  nacsfix  29001  fnwe2lem2  29357  kelac1  29369  unxpwdom3  29401  hbtlem5  29437  hbt  29439  dgraa0p  29459  hashgcdeq  29519  rlimdmafv  30036  numclwwlkovf2ex  30632  mat1dimcrng  30796  mdetdiaglem  30824  lindslinindsimp2  30886  atlatmstc  32804  cvrexchlem  32903  paddasslem14  33317  pexmidlem5N  33458  cdleme29ex  33858  cdlemefr29exN  33886  cdleme32fva  33921  diarnN  34614  dihlsscpre  34719
  Copyright terms: Public domain W3C validator