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

Theorem expr 618
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 608 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 430 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  reximddv  2908  rexlimdvaa  2925  disjxiun  4423  wereu2  4851  fcof1  6200  knatar  6263  riota5f  6291  ovmpt2df  6442  extmptsuppeq  6950  suppss  6956  suppss2  6960  wfrlem17  7060  smoord  7092  tfrlem9a  7112  oaass  7270  oelimcl  7309  oaabs2  7354  swoso  7402  eceqoveq  7476  domdifsn  7661  domunsncan  7678  omxpenlem  7679  enfixsn  7687  mapdom2  7749  frfi  7822  fofinf1o  7858  finsschain  7887  elfiun  7950  marypha1lem  7953  eqsupd  7977  eqinfd  8007  ordiso2  8030  ordtypelem6  8038  ordtypelem7  8039  ordtypelem10  8042  oismo  8055  wemapsolem  8065  brwdom2  8088  wdomtr  8090  unwdomg  8099  xpwdomg  8100  unxpwdom2  8103  cantnfval2  8173  cantnfle  8175  cantnflem1  8193  cantnf  8197  r1ordg  8248  tcrank  8354  carddomi2  8403  harval2  8430  infxpenlem  8443  infxpenc2lem2  8449  fseqenlem1  8453  dfac8clem  8461  acndom2  8483  infpwfien  8491  iunfictbso  8543  dfac12lem3  8573  infxp  8643  coflim  8689  cofsmo  8697  coftr  8701  sornom  8705  infpssrlem4  8734  enfin2i  8749  fin23lem26  8753  fin23lem27  8756  fin23lem36  8776  fin23lem40  8779  isf32lem5  8785  isf34lem4  8805  isfin1-3  8814  fin1a2lem10  8837  fin1a2lem13  8840  fin1a2s  8842  hsmexlem4  8857  ttukeylem5  8941  ttukeylem6  8942  ttukeylem7  8943  alephval2  8995  gchor  9051  fpwwe2lem7  9060  fpwwe2lem12  9065  fpwwe2  9067  pwfseqlem4a  9085  pwfseqlem4  9086  winalim2  9120  gchina  9123  inar1  9199  nqereq  9359  prlem934  9457  prlem936  9471  addsrmo  9496  mulsrmo  9497  supsrlem  9534  axpre-sup  9592  dedekind  9796  dedekindle  9797  prodge0  10451  mulge0b  10474  supaddc  10574  supmul1  10576  un0addcl  10903  un0mulcl  10904  uzwo3  11259  qbtwnre  11492  xlemul1a  11574  seqcl2  12228  seqfveq2  12232  seqshft2  12236  monoord  12240  seqsplit  12243  seqf1olem1  12249  seqid2  12256  seqhomo  12257  expnegz  12303  expcan  12322  ltexp2  12323  discr  12406  bcval5  12500  hashbc  12611  hashf1lem2  12614  seqcoll  12621  seqcoll2  12622  wrdind  12818  wrd2ind  12819  cau3lem  13396  ello1d  13565  lo1bdd2  13566  rlimclim  13588  climrlim2  13589  rlimdm  13593  rlimcn1  13630  reccn2  13638  rlimsqzlem  13690  lo1le  13693  caucvgrlem  13714  caucvgrlemOLD  13715  caurcvg2  13722  summolem2  13760  zsum  13762  fsum  13764  fsumf1o  13767  sumss  13768  fsumss  13769  fsumcl2lem  13775  fsumadd  13783  fsumcom2  13813  fsum0diag2  13822  fsummulc2  13823  fsumconst  13829  fsumrelem  13845  fsumrlim  13849  fsumo1  13850  divrcnv  13888  geomulcvg  13910  mertenslem2  13919  prodmolem2  13967  zprod  13969  fprod  13973  fprodf1o  13978  prodss  13979  fprodss  13980  fprodcl2lem  13982  fprodmul  13992  fproddiv  13993  fprodconst  14010  fprodn0  14011  fprodcom2  14016  ruclem8  14267  dvds0lem  14291  dvdsnegb  14298  dvdssub2  14320  bitsf1  14394  bitsshft  14423  bezoutlem3  14479  bezoutlem4  14480  isprm2lem  14593  isprm5  14613  isprm6  14628  modprminv  14704  modprminveq  14705  reumodprminv  14709  pcqmul  14757  pcqcl  14760  pcxcl  14764  pc2dvds  14782  pcadd  14788  pcmpt  14791  pockthg  14804  infpnlem1  14808  prmreclem5  14818  vdwlem2  14886  vdwlem9  14893  vdwlem10  14894  vdwlem12  14896  ramub  14924  0ram  14932  ramub1lem2  14939  ramub1  14940  ramcl  14941  mreexexd  15496  acsfn2  15511  iscatd  15521  catpropd  15556  setcmon  15924  pleval2i  16152  psss  16402  mgmidsssn0  16454  mhmeql  16553  frmdss2  16589  frmdup3  16593  grprcan  16641  mulgnn0ass  16729  isnsg3  16793  ghmpreima  16846  ghmeql  16847  gaorber  16904  f1omvdco2  17031  psgnunilem1  17076  psgnunilem2  17078  oddvds  17129  gexdvds  17162  sylow1lem1  17176  odcau  17182  pgpssslw  17192  sylow2alem2  17196  sylow2blem3  17200  fislw  17203  lsmmod  17251  efgredlem  17323  frgpup3  17354  gsumval3  17467  gsumzres  17469  gsumzcl2  17470  gsumzf1o  17472  gsumzaddlem  17480  gsumconst  17493  gsumzmhm  17496  gsumzoppg  17503  gsum2d2lem  17531  ablfac1eulem  17631  pgpfac1lem5  17638  ablfaclem3  17646  issubdrg  17959  lss1d  18112  lmhmeql  18204  lspextmo  18205  lspsnat  18294  lsppratlem6  18301  islbs3  18304  lbsextlem4  18310  lidl1el  18368  mvrf1  18575  mplsubglem  18584  mpllsslem  18585  mplcoe1  18615  mplcoe5  18618  gsummoncoe1  18824  cnsubrg  18954  gsumfsum  18960  prmirredlem  18986  znidomb  19054  frgpcyg  19066  cssmre  19178  dsmmsubg  19228  dsmmlss  19229  frlmsslsp  19276  lindff1  19300  lindfrn  19301  mat1dimcrng  19424  mdetdiaglem  19545  mdetunilem7  19565  mdetunilem8  19566  mdetunilem9  19567  cpmatacl  19662  cpmatmcllem  19664  mp2pm2mplem4  19755  en2top  19923  toponmre  20031  topssnei  20062  innei  20063  clslp  20086  restcls  20119  restntr  20120  ordtrest2lem  20141  cnpco  20205  cncls2  20211  cncnpi  20216  cncnp  20218  cnconst2  20221  cnpdis  20231  lmcnp  20242  cnhaus  20292  isreg2  20315  cncmp  20329  tgcmp  20338  sscmp  20342  cmpfi  20345  cnconn  20359  iunconlem  20364  clscon  20367  1stcfb  20382  1stcrest  20390  2ndcctbss  20392  2ndcdisj  20393  1stcelcls  20398  1stccnp  20399  restnlly  20419  cldllycmp  20432  lly1stc  20433  dislly  20434  locfincmp  20463  comppfsc  20469  kgentopon  20475  kgenidm  20484  1stckgenlem  20490  kgencn3  20495  ptpjpre1  20508  ptbasin  20514  txcls  20541  tx2cn  20547  ptpjcn  20548  ptclsg  20552  ptcnp  20559  txdis  20569  txlly  20573  txnlly  20574  pthaus  20575  txtube  20577  txcmplem1  20578  txcmplem2  20579  txcmp  20580  txhaus  20584  txkgen  20589  xkohaus  20590  xkococnlem  20596  xkococn  20597  txcon  20626  qtopeu  20653  qtoprest  20654  regr1lem2  20677  kqreglem1  20678  cmphaushmeo  20737  xkocnv  20751  fgabs  20816  filuni  20822  trufil  20847  ufileu  20856  filufint  20857  fin1aufil  20869  elfm2  20885  rnelfmlem  20889  fmfnfmlem2  20892  fmfnfmlem4  20894  fmufil  20896  flimopn  20912  fbflim2  20914  hausflimi  20917  hausflim  20918  flimcf  20919  flimclslem  20921  flimsncls  20923  hauspwpwf1  20924  cnpflfi  20936  fclsnei  20956  fclscf  20962  flimfnfcls  20965  fclscmp  20967  ufilcmp  20969  fcfnei  20972  cnpfcf  20978  alexsublem  20981  alexsub  20982  alexsubALTlem2  20985  alexsubALTlem3  20986  alexsubALTlem4  20987  ptcmplem3  20991  ptcmplem4  20992  ptcmplem5  20993  symgtgp  21038  tgpconcompeqg  21048  tgpconcomp  21049  ghmcnp  21051  tgpt0  21055  qustgplem  21057  haustsms2  21073  tsmsgsum  21075  tsmsres  21080  tsmsxp  21091  imasdsf1olem  21310  xbln0  21351  blssps  21361  blss  21362  neibl  21438  blcld  21442  metss  21445  metequiv2  21447  met1stc  21458  metrest  21461  prdsxmslem2  21466  metcnp3  21477  nrmmetd  21511  nlmvscnlem1  21611  nrginvrcnlem  21615  nmoleub  21654  icccmplem2  21743  icccmp  21745  reconnlem2  21747  xrge0tsms  21754  metdstri  21770  metdseq0  21773  metdscn  21775  cnmpt2pc  21843  lebnumlem3  21878  pcoval2  21931  pcopt  21937  nmoleub2lem  22012  nmhmcn  22018  ipcnlem1  22100  cfilfcls  22128  cmetcaulem  22142  iscmet3lem2  22146  iscmet3  22147  equivcau  22154  caubl  22161  bcthlem2  22177  bcthlem3  22178  bcthlem4  22179  bcthlem5  22180  ivthlem2  22275  ivthlem3  22276  ovoliunlem2  22325  ovolicc2lem2  22340  ovolicc2lem3  22341  ovolicc2lem5  22343  ovolicc2  22344  ismbl2  22349  nulmbl  22357  nulmbl2  22358  unmbl  22359  shftmbl  22360  voliunlem3  22373  volsup  22377  ioombl1lem4  22382  ioombl1  22383  icombl  22385  ioombl  22386  uniioombl  22415  opnmbllem  22427  volivth  22433  vitali  22439  mbflimsup  22491  mbflimsupOLD  22492  i1fadd  22521  itg1addlem4  22525  itg2le  22565  itg2seq  22568  itg2lea  22570  itg2splitlem  22574  itg2split  22575  itg2mono  22579  itg2gt0  22586  itg2cnlem2  22588  itgss  22637  itgfsum  22652  itgcn  22668  ellimc3  22702  limcco  22716  limciun  22717  dvnres  22753  dvnfre  22774  rolle  22810  c1liplem1  22816  dvivth  22830  dvne0  22831  lhop1lem  22833  lhop1  22834  lhop  22836  dvcnvrelem1  22837  dvfsumrlim  22851  dvfsum2  22854  ftc1a  22857  ftc1lem6  22861  itgsubst  22869  tdeglem4  22877  mdegaddle  22891  mdegvscale  22892  mdegmullem  22895  deg1tmle  22934  ply1divex  22953  dvdsq1p  22977  fta1g  22984  fta1b  22986  plyco0  23005  coeeulem  23037  dgrlem  23042  plyco  23054  coemullem  23063  dgreq0  23078  dgrco  23088  plydivex  23109  quotcan  23121  aannenlem1  23140  aalioulem2  23145  aalioulem3  23146  taylthlem1  23184  ulmbdd  23209  itgulm  23219  radcnvlt1  23229  psercnlem1  23236  abelthlem2  23243  abelthlem8  23250  logcnlem5  23447  efopn  23459  cxpmul2z  23492  cxpcn3lem  23543  cxpeq  23553  xrlimcnp  23750  cxplim  23753  o1cxp  23756  cxploglim  23759  scvxcvx  23767  jensen  23770  ftalem1  23853  ftalem2  23854  fta  23860  basellem3  23863  isppw2  23896  ppinprm  23933  chtnprm  23935  dvdsmulf1o  23977  chtublem  23993  perfectlem2  24012  dchrfi  24037  dchrptlem1  24046  dchrptlem2  24047  dchrptlem3  24048  dchrsum2  24050  bposlem1  24066  bposlem3  24068  2sqlem5  24150  2sqlem6  24151  2sqlem8  24154  2sqlem10  24156  2sqb  24160  chebbnd1lem1  24161  chtppilimlem2  24166  dchrisum0flb  24202  dchrisum0fno1  24203  dchrisum0  24212  pntrsumbnd2  24259  pntpbnd1  24278  pntpbnd2  24279  pntlemp  24302  pnt3  24304  qabvle  24317  ostth2lem2  24326  ostth3  24330  ostth  24331  colinearalglem4  24776  axcontlem10  24840  umgraex  24887  eupai  25531  numclwwlkovf2ex  25650  isgrp2d  25799  ghgrpOLD  25932  ghabloOLD  25933  smcnlem  26169  ubthlem1  26348  ubthlem3  26350  htthlem  26396  5oalem6  27138  leopmuli  27612  pjnormssi  27647  pjclem4  27678  pj3si  27686  hatomistici  27841  sumdmdlem  27897  suppss2fOLD  28068  xrge0tsmsd  28378  isarchiofld  28410  ordtrest2NEWlem  28558  qqhf  28620  eulerpartlemb  29018  ballotlemfc0  29142  ballotlemfcc  29143  sgn3da  29191  subfacp1lem5  29686  erdszelem7  29699  erdszelem11  29703  pconcon  29733  txpcon  29734  conpcon  29737  sconpi1  29741  txscon  29743  cvxscon  29745  cvmopnlem  29780  cvmfolem  29781  cvmliftmolem2  29784  cvmliftlem7  29793  cvmliftlem10  29796  cvmlift2lem10  29814  cvmlift3lem4  29824  cvmlift3lem8  29828  msubff1  29973  wzel  30285  wsuclem  30286  nofulllem4  30370  btwnouttr2  30565  cgrxfr  30598  btwnxfr  30599  brcolinear  30602  lineext  30619  btwnconn1lem13  30642  midofsegid  30647  segcon2  30648  brsegle  30651  seglecgr12im  30653  segletr  30657  colinbtwnle  30661  broutsideof2  30665  btwnoutside  30668  broutsideof3  30669  outsideoftr  30672  outsideofeq  30673  outsideofeu  30674  outsidele  30675  lineunray  30690  lineelsb2  30691  linethru  30696  finminlem  30750  nn0prpwlem  30754  neibastop2lem  30792  neibastop2  30793  neibastop3  30794  topjoin  30797  tailfb  30809  relowlssretop  31491  wl-sbcom2d-lem1  31587  finixpnum  31624  poimirlem6  31640  poimirlem7  31641  poimirlem13  31647  poimirlem26  31660  poimirlem29  31663  heicant  31669  opnmbllem0  31670  mblfinlem3  31673  ismblfin  31675  ovoliunnfl  31676  voliunnfl  31678  volsupnfl  31679  itg2addnclem  31687  itg2addnclem3  31689  ftc1cnnc  31710  sdclem2  31765  fdc  31768  istotbnd3  31797  isbnd2  31809  isbnd3  31810  prdsbnd  31819  cntotbnd  31822  heibor1lem  31835  heibor1  31836  heiborlem10  31846  rrncmslem  31858  ghomco  31875  1idl  31953  unichnidl  31958  prtlem10  32135  prtlem18  32147  atlatmstc  32584  cvrexchlem  32683  paddasslem14  33097  pexmidlem5N  33238  cdleme29ex  33640  cdlemefr29exN  33668  cdleme32fva  33703  diarnN  34396  dihlsscpre  34501  isnacs3  35251  fnwe2lem2  35605  kelac1  35617  hbtlem5  35683  hbt  35685  dgraa0p  35704  hashgcdeq  35764  rlimdmafv  38059  smonoord  38098  perfectALTVlem2  38224  mgmhmeql  38551  lindslinindsimp2  39006
  Copyright terms: Public domain W3C validator