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  2919  rexlimdvaa  2936  disjxiun  4434  wereu2  4866  suppssOLD  6005  fcof1  6175  knatar  6238  riota5f  6267  ovmpt2df  6419  suppss2OLD  6515  extmptsuppeq  6926  suppss  6932  suppss2  6936  smoord  7038  tfrlem9a  7057  oaass  7212  oelimcl  7251  oaabs2  7296  swoso  7344  eceqoveq  7418  domdifsn  7602  domunsncan  7619  omxpenlem  7620  enfixsn  7628  mapdom2  7690  frfi  7767  fofinf1o  7803  finsschain  7829  elfiun  7892  marypha1lem  7895  eqsupd  7919  ordiso2  7943  ordtypelem6  7951  ordtypelem7  7952  ordtypelem10  7955  oismo  7968  wemapsolem  7978  brwdom2  8002  wdomtr  8004  unwdomg  8013  xpwdomg  8014  unxpwdom2  8017  cantnfval2  8091  cantnfle  8093  cantnflem1  8111  cantnf  8115  cantnfval2OLD  8121  cantnfleOLD  8123  cantnflem1OLD  8134  cantnfOLD  8137  r1ordg  8199  tcrank  8305  carddomi2  8354  harval2  8381  infxpenlem  8394  infxpenc2lem2  8400  infxpenc2lem2OLD  8404  fseqenlem1  8408  dfac8clem  8416  acndom2  8438  infpwfien  8446  iunfictbso  8498  dfac12lem3  8528  infxp  8598  coflim  8644  cofsmo  8652  coftr  8656  sornom  8660  infpssrlem4  8689  enfin2i  8704  fin23lem26  8708  fin23lem27  8711  fin23lem36  8731  fin23lem40  8734  isf32lem5  8740  isf34lem4  8760  isfin1-3  8769  fin1a2lem10  8792  fin1a2lem13  8795  fin1a2s  8797  hsmexlem4  8812  ttukeylem5  8896  ttukeylem6  8897  ttukeylem7  8898  alephval2  8950  gchor  9008  fpwwe2lem7  9017  fpwwe2lem12  9022  fpwwe2  9024  pwfseqlem4a  9042  pwfseqlem4  9043  winalim2  9077  gchina  9080  inar1  9156  nqereq  9316  prlem934  9414  prlem936  9428  addsrmo  9453  mulsrmo  9454  supsrlem  9491  axpre-sup  9549  dedekind  9747  dedekindle  9748  prodge0  10396  mulge0b  10419  supmul1  10515  un0addcl  10836  un0mulcl  10837  uzwo3  11188  qbtwnre  11409  xlemul1a  11491  seqcl2  12107  seqfveq2  12111  seqshft2  12115  monoord  12119  seqsplit  12122  seqf1olem1  12128  seqid2  12135  seqhomo  12136  expnegz  12182  expcan  12200  ltexp2  12201  discr  12285  bcval5  12378  hashbc  12484  hashf1lem2  12487  seqcoll  12494  seqcoll2  12495  wrdind  12684  wrd2ind  12685  cau3lem  13169  ello1d  13328  lo1bdd2  13329  rlimclim  13351  climrlim2  13352  rlimdm  13356  rlimcn1  13393  reccn2  13401  rlimsqzlem  13453  lo1le  13456  caucvgrlem  13477  caurcvg2  13482  summolem2  13520  zsum  13522  fsum  13524  fsumf1o  13527  sumss  13528  fsumss  13529  fsumcl2lem  13535  fsumadd  13543  fsumcom2  13571  fsum0diag2  13580  fsummulc2  13581  fsumconst  13587  fsumrelem  13603  fsumrlim  13607  fsumo1  13608  divrcnv  13646  geomulcvg  13667  mertenslem2  13676  prodmolem2  13724  zprod  13726  fprod  13730  fprodf1o  13735  prodss  13736  fprodss  13737  fprodcl2lem  13739  fprodmul  13747  fproddiv  13748  fprodconst  13764  fprodn0  13765  fprodcom2  13770  ruclem8  13952  dvds0lem  13976  dvdsnegb  13983  dvdssub2  14005  bitsf1  14078  bitsshft  14107  bezoutlem3  14160  bezoutlem4  14161  isprm2lem  14206  isprm6  14232  isprm5  14235  modprminv  14308  modprminveq  14309  reumodprminv  14311  pcqmul  14359  pcqcl  14362  pcxcl  14366  pc2dvds  14384  pcadd  14390  pcmpt  14393  pockthg  14406  infpnlem1  14410  prmreclem5  14420  vdwlem2  14482  vdwlem9  14489  vdwlem10  14490  vdwlem12  14492  ramub  14513  0ram  14520  ramub1lem2  14527  ramub1  14528  ramcl  14529  mreexexd  15027  acsfn2  15042  iscatd  15052  catpropd  15086  setcmon  15393  pleval2i  15573  psss  15823  mgmidsssn0  15875  mhmeql  15974  frmdss2  16010  frmdup3  16014  grprcan  16062  mulgnn0ass  16150  isnsg3  16214  ghmpreima  16267  ghmeql  16268  gaorber  16325  f1omvdco2  16452  psgnunilem1  16497  psgnunilem2  16499  oddvds  16550  gexdvds  16583  sylow1lem1  16597  odcau  16603  pgpssslw  16613  sylow2alem2  16617  sylow2blem3  16621  fislw  16624  lsmmod  16672  efgredlem  16744  frgpup3  16775  gsumval3OLD  16887  gsumval3  16890  gsumzres  16893  gsumzcl2  16894  gsumzf1o  16896  gsumzresOLD  16897  gsumzclOLD  16898  gsumzf1oOLD  16899  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumconst  16933  gsumzmhm  16936  gsumzmhmOLD  16937  gsumzoppg  16946  gsumzoppgOLD  16947  gsum2d2lem  16980  ablfac1eulem  17102  pgpfac1lem5  17109  ablfaclem3  17117  issubdrg  17433  lss1d  17588  lmhmeql  17680  lspextmo  17681  lspsnat  17770  lsppratlem6  17777  islbs3  17780  lbsextlem4  17786  lidl1el  17845  mvrf1  18060  mplsubglem  18072  mpllsslem  18073  mplsubglemOLD  18074  mpllsslemOLD  18075  mplcoe1  18106  mplcoe5  18110  mplcoe2OLD  18112  gsummoncoe1  18325  cnsubrg  18457  gsumfsum  18463  prmirredlem  18501  prmirredlemOLD  18504  znidomb  18578  frgpcyg  18590  cssmre  18702  dsmmsubg  18752  dsmmlss  18753  frlmsslsp  18807  frlmsslspOLD  18808  lindff1  18833  lindfrn  18834  mat1dimcrng  18957  mdetdiaglem  19078  mdetunilem7  19098  mdetunilem8  19099  mdetunilem9  19100  cpmatacl  19195  cpmatmcllem  19197  mp2pm2mplem4  19288  en2top  19465  toponmre  19572  topssnei  19603  innei  19604  clslp  19627  restcls  19660  restntr  19661  ordtrest2lem  19682  cnpco  19746  cncls2  19752  cncnpi  19757  cncnp  19759  cnconst2  19762  cnpdis  19772  lmcnp  19783  cnhaus  19833  isreg2  19856  cncmp  19870  tgcmp  19879  sscmp  19883  cmpfi  19886  cnconn  19901  iunconlem  19906  clscon  19909  1stcfb  19924  1stcrest  19932  2ndcctbss  19934  2ndcdisj  19935  1stcelcls  19940  1stccnp  19941  restnlly  19961  cldllycmp  19974  lly1stc  19975  dislly  19976  locfincmp  20005  comppfsc  20011  kgentopon  20017  kgenidm  20026  1stckgenlem  20032  kgencn3  20037  ptpjpre1  20050  ptbasin  20056  txcls  20083  tx2cn  20089  ptpjcn  20090  ptclsg  20094  ptcnp  20101  txdis  20111  txlly  20115  txnlly  20116  pthaus  20117  txtube  20119  txcmplem1  20120  txcmplem2  20121  txcmp  20122  txhaus  20126  txkgen  20131  xkohaus  20132  xkococnlem  20138  xkococn  20139  txcon  20168  qtopeu  20195  qtoprest  20196  regr1lem2  20219  kqreglem1  20220  cmphaushmeo  20279  xkocnv  20293  fgabs  20358  filuni  20364  trufil  20389  ufileu  20398  filufint  20399  fin1aufil  20411  elfm2  20427  rnelfmlem  20431  fmfnfmlem2  20434  fmfnfmlem4  20436  fmufil  20438  flimopn  20454  fbflim2  20456  hausflimi  20459  hausflim  20460  flimcf  20461  flimclslem  20463  flimsncls  20465  hauspwpwf1  20466  cnpflfi  20478  fclsnei  20498  fclscf  20504  flimfnfcls  20507  fclscmp  20509  ufilcmp  20511  fcfnei  20514  cnpfcf  20520  alexsublem  20522  alexsub  20523  alexsubALTlem2  20526  alexsubALTlem3  20527  alexsubALTlem4  20528  ptcmplem3  20532  ptcmplem4  20533  ptcmplem5  20534  symgtgp  20578  tgpconcompeqg  20588  tgpconcomp  20589  ghmcnp  20591  tgpt0  20595  qustgplem  20597  haustsms2  20613  tsmsgsum  20615  tsmsgsumOLD  20618  tsmsresOLD  20623  tsmsres  20624  tsmsxp  20635  imasdsf1olem  20854  xbln0  20895  blssps  20905  blss  20906  neibl  20982  blcld  20986  metss  20989  metequiv2  20991  met1stc  21002  metrest  21005  prdsxmslem2  21010  metcnp3  21021  nrmmetd  21073  nlmvscnlem1  21173  nrginvrcnlem  21177  nmoleub  21216  icccmplem2  21306  icccmp  21308  reconnlem2  21310  xrge0tsms  21317  metdstri  21333  metdseq0  21336  metdscn  21338  cnmpt2pc  21406  lebnumlem3  21441  pcoval2  21494  pcopt  21500  nmoleub2lem  21575  nmhmcn  21581  ipcnlem1  21663  cfilfcls  21691  cmetcaulem  21705  iscmet3lem2  21709  iscmet3  21710  equivcau  21717  caubl  21724  bcthlem2  21742  bcthlem3  21743  bcthlem4  21744  bcthlem5  21745  ivthlem2  21842  ivthlem3  21843  ovoliunlem2  21892  ovolicc2lem2  21907  ovolicc2lem3  21908  ovolicc2lem5  21910  ovolicc2  21911  ismbl2  21916  nulmbl  21924  nulmbl2  21925  unmbl  21926  shftmbl  21927  voliunlem3  21940  volsup  21944  ioombl1lem4  21949  ioombl1  21950  icombl  21952  ioombl  21953  uniioombl  21976  opnmbllem  21988  volivth  21994  vitali  22000  mbflimsup  22051  i1fadd  22080  itg1addlem4  22084  itg2le  22124  itg2seq  22127  itg2lea  22129  itg2splitlem  22133  itg2split  22134  itg2mono  22138  itg2gt0  22145  itg2cnlem2  22147  itgss  22196  itgfsum  22211  itgcn  22227  ellimc3  22261  limcco  22275  limciun  22276  dvnres  22312  dvnfre  22333  rolle  22369  c1liplem1  22375  dvivth  22389  dvne0  22390  lhop1lem  22392  lhop1  22393  lhop  22395  dvcnvrelem1  22396  dvfsumrlim  22410  dvfsum2  22413  ftc1a  22416  ftc1lem6  22420  itgsubst  22428  tdeglem4  22436  mdegaddle  22452  mdegvscale  22453  mdegmullem  22456  deg1tmle  22496  ply1divex  22515  dvdsq1p  22539  fta1g  22546  fta1b  22548  plyco0  22567  coeeulem  22599  dgrlem  22604  plyco  22616  coemullem  22625  dgreq0  22640  dgrco  22650  plydivex  22671  quotcan  22683  aannenlem1  22702  aalioulem2  22707  aalioulem3  22708  taylthlem1  22746  ulmbdd  22771  itgulm  22781  radcnvlt1  22791  psercnlem1  22798  abelthlem2  22805  abelthlem8  22812  logcnlem5  23005  efopn  23017  cxpmul2z  23050  cxpcn3lem  23099  cxpeq  23109  xrlimcnp  23276  cxplim  23279  o1cxp  23282  cxploglim  23285  scvxcvx  23293  jensen  23296  ftalem1  23324  ftalem2  23325  fta  23331  basellem3  23334  isppw2  23367  ppinprm  23404  chtnprm  23406  dvdsmulf1o  23448  chtublem  23464  perfectlem2  23483  dchrfi  23508  dchrptlem1  23517  dchrptlem2  23518  dchrptlem3  23519  dchrsum2  23521  bposlem1  23537  bposlem3  23539  2sqlem5  23621  2sqlem6  23622  2sqlem8  23625  2sqlem10  23627  2sqb  23631  chebbnd1lem1  23632  chtppilimlem2  23637  dchrisum0flb  23673  dchrisum0fno1  23674  dchrisum0  23683  pntrsumbnd2  23730  pntpbnd1  23749  pntpbnd2  23750  pntlemp  23773  pnt3  23775  qabvle  23788  ostth2lem2  23797  ostth3  23801  ostth  23802  colinearalglem4  24190  axcontlem10  24254  umgraex  24301  eupai  24945  numclwwlkovf2ex  25064  isgrp2d  25215  ghgrpOLD  25348  ghabloOLD  25349  smcnlem  25585  ubthlem1  25764  ubthlem3  25766  htthlem  25812  5oalem6  26555  leopmuli  27030  pjnormssi  27065  pjclem4  27096  pj3si  27104  hatomistici  27259  sumdmdlem  27315  suppss2f  27455  xrge0tsmsd  27753  isarchiofld  27785  ordtrest2NEWlem  27882  qqhf  27945  eulerpartlemb  28285  ballotlemfc0  28409  ballotlemfcc  28410  sgn3da  28458  subfacp1lem5  28606  erdszelem7  28619  erdszelem11  28623  pconcon  28654  txpcon  28655  conpcon  28658  sconpi1  28662  txscon  28664  cvxscon  28666  cvmopnlem  28701  cvmfolem  28702  cvmliftmolem2  28705  cvmliftlem7  28714  cvmliftlem10  28717  cvmlift2lem10  28735  cvmlift3lem4  28745  cvmlift3lem8  28749  msubff1  28894  wzel  29356  wsuclem  29357  nofulllem4  29441  btwnouttr2  29648  cgrxfr  29681  btwnxfr  29682  brcolinear  29685  lineext  29702  btwnconn1lem13  29725  midofsegid  29730  segcon2  29731  brsegle  29734  seglecgr12im  29736  segletr  29740  colinbtwnle  29744  broutsideof2  29748  btwnoutside  29751  broutsideof3  29752  outsideoftr  29755  outsideofeq  29756  outsideofeu  29757  outsidele  29758  lineunray  29773  lineelsb2  29774  linethru  29779  wl-sbcom2d-lem1  29985  finixpnum  30014  supaddc  30017  heicant  30025  opnmbllem0  30026  mblfinlem3  30029  ismblfin  30031  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  itg2addnclem  30042  itg2addnclem3  30044  ftc1cnnc  30065  finminlem  30112  nn0prpwlem  30116  neibastop2lem  30154  neibastop2  30155  neibastop3  30156  topjoin  30159  tailfb  30171  sdclem2  30211  fdc  30214  istotbnd3  30243  isbnd2  30255  isbnd3  30256  prdsbnd  30265  cntotbnd  30268  heibor1lem  30281  heibor1  30282  heiborlem10  30292  rrncmslem  30304  ghomco  30321  1idl  30399  unichnidl  30404  prtlem10  30582  prtlem18  30594  isnacs3  30618  fnwe2lem2  30973  kelac1  30985  hbtlem5  31053  hbt  31055  dgraa0p  31074  hashgcdeq  31134  rlimdmafv  32216  mgmhmeql  32445  lindslinindsimp2  32934  atlatmstc  34919  cvrexchlem  35018  paddasslem14  35432  pexmidlem5N  35573  cdleme29ex  35975  cdlemefr29exN  36003  cdleme32fva  36038  diarnN  36731  dihlsscpre  36836
  Copyright terms: Public domain W3C validator