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

Theorem expr 613
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 603 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 427 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  reximddv  2858  rexlimdvaa  2875  disjxiun  4364  wereu2  4790  suppssOLD  5922  fcof1  6091  knatar  6154  riota5f  6182  ovmpt2df  6333  suppss2OLD  6429  extmptsuppeq  6842  suppss  6848  suppss2  6852  smoord  6954  tfrlem9a  6973  oaass  7128  oelimcl  7167  oaabs2  7212  swoso  7260  eceqoveq  7334  domdifsn  7519  domunsncan  7536  omxpenlem  7537  enfixsn  7545  mapdom2  7607  frfi  7680  fofinf1o  7716  finsschain  7742  elfiun  7805  marypha1lem  7808  eqsupd  7831  ordiso2  7855  ordtypelem6  7863  ordtypelem7  7864  ordtypelem10  7867  oismo  7880  wemapsolem  7890  brwdom2  7914  wdomtr  7916  unwdomg  7925  xpwdomg  7926  unxpwdom2  7929  cantnfval2  8001  cantnfle  8003  cantnflem1  8021  cantnf  8025  cantnfval2OLD  8031  cantnfleOLD  8033  cantnflem1OLD  8044  cantnfOLD  8047  r1ordg  8109  tcrank  8215  carddomi2  8264  harval2  8291  infxpenlem  8304  infxpenc2lem2  8310  infxpenc2lem2OLD  8314  fseqenlem1  8318  dfac8clem  8326  acndom2  8348  infpwfien  8356  iunfictbso  8408  dfac12lem3  8438  infxp  8508  coflim  8554  cofsmo  8562  coftr  8566  sornom  8570  infpssrlem4  8599  enfin2i  8614  fin23lem26  8618  fin23lem27  8621  fin23lem36  8641  fin23lem40  8644  isf32lem5  8650  isf34lem4  8670  isfin1-3  8679  fin1a2lem10  8702  fin1a2lem13  8705  fin1a2s  8707  hsmexlem4  8722  ttukeylem5  8806  ttukeylem6  8807  ttukeylem7  8808  alephval2  8860  gchor  8916  fpwwe2lem7  8925  fpwwe2lem12  8930  fpwwe2  8932  pwfseqlem4a  8950  pwfseqlem4  8951  winalim2  8985  gchina  8988  inar1  9064  nqereq  9224  prlem934  9322  prlem936  9336  addsrmo  9361  mulsrmo  9362  supsrlem  9399  axpre-sup  9457  dedekind  9655  dedekindle  9656  prodge0  10306  mulge0b  10329  supmul1  10424  un0addcl  10746  un0mulcl  10747  uzwo3  11096  qbtwnre  11319  xlemul1a  11401  seqcl2  12028  seqfveq2  12032  seqshft2  12036  monoord  12040  seqsplit  12043  seqf1olem1  12049  seqid2  12056  seqhomo  12057  expnegz  12103  expcan  12121  ltexp2  12122  discr  12205  bcval5  12298  hashbc  12406  hashf1lem2  12409  seqcoll  12416  seqcoll2  12417  wrdind  12613  wrd2ind  12614  cau3lem  13189  ello1d  13348  lo1bdd2  13349  rlimclim  13371  climrlim2  13372  rlimdm  13376  rlimcn1  13413  reccn2  13421  rlimsqzlem  13473  lo1le  13476  caucvgrlem  13497  caurcvg2  13502  summolem2  13540  zsum  13542  fsum  13544  fsumf1o  13547  sumss  13548  fsumss  13549  fsumcl2lem  13555  fsumadd  13563  fsumcom2  13591  fsum0diag2  13600  fsummulc2  13601  fsumconst  13607  fsumrelem  13623  fsumrlim  13627  fsumo1  13628  divrcnv  13666  geomulcvg  13687  mertenslem2  13696  prodmolem2  13744  zprod  13746  fprod  13750  fprodf1o  13755  prodss  13756  fprodss  13757  fprodcl2lem  13759  fprodmul  13767  fproddiv  13768  fprodconst  13784  fprodn0  13785  fprodcom2  13790  ruclem8  13972  dvds0lem  13996  dvdsnegb  14003  dvdssub2  14025  bitsf1  14098  bitsshft  14127  bezoutlem3  14180  bezoutlem4  14181  isprm2lem  14226  isprm6  14252  isprm5  14255  modprminv  14328  modprminveq  14329  reumodprminv  14331  pcqmul  14379  pcqcl  14382  pcxcl  14386  pc2dvds  14404  pcadd  14410  pcmpt  14413  pockthg  14426  infpnlem1  14430  prmreclem5  14440  vdwlem2  14502  vdwlem9  14509  vdwlem10  14510  vdwlem12  14512  ramub  14533  0ram  14540  ramub1lem2  14547  ramub1  14548  ramcl  14549  mreexexd  15055  acsfn2  15070  iscatd  15080  catpropd  15115  setcmon  15483  pleval2i  15711  psss  15961  mgmidsssn0  16013  mhmeql  16112  frmdss2  16148  frmdup3  16152  grprcan  16200  mulgnn0ass  16288  isnsg3  16352  ghmpreima  16405  ghmeql  16406  gaorber  16463  f1omvdco2  16590  psgnunilem1  16635  psgnunilem2  16637  oddvds  16688  gexdvds  16721  sylow1lem1  16735  odcau  16741  pgpssslw  16751  sylow2alem2  16755  sylow2blem3  16759  fislw  16762  lsmmod  16810  efgredlem  16882  frgpup3  16913  gsumval3OLD  17025  gsumval3  17028  gsumzres  17031  gsumzcl2  17032  gsumzf1o  17034  gsumzresOLD  17035  gsumzclOLD  17036  gsumzf1oOLD  17037  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsumconst  17070  gsumzmhm  17073  gsumzmhmOLD  17074  gsumzoppg  17083  gsumzoppgOLD  17084  gsum2d2lem  17115  ablfac1eulem  17236  pgpfac1lem5  17243  ablfaclem3  17251  issubdrg  17567  lss1d  17722  lmhmeql  17814  lspextmo  17815  lspsnat  17904  lsppratlem6  17911  islbs3  17914  lbsextlem4  17920  lidl1el  17979  mvrf1  18194  mplsubglem  18206  mpllsslem  18207  mplsubglemOLD  18208  mpllsslemOLD  18209  mplcoe1  18240  mplcoe5  18244  mplcoe2OLD  18246  gsummoncoe1  18459  cnsubrg  18591  gsumfsum  18597  prmirredlem  18623  znidomb  18691  frgpcyg  18703  cssmre  18815  dsmmsubg  18865  dsmmlss  18866  frlmsslsp  18916  lindff1  18940  lindfrn  18941  mat1dimcrng  19064  mdetdiaglem  19185  mdetunilem7  19205  mdetunilem8  19206  mdetunilem9  19207  cpmatacl  19302  cpmatmcllem  19304  mp2pm2mplem4  19395  en2top  19572  toponmre  19680  topssnei  19711  innei  19712  clslp  19735  restcls  19768  restntr  19769  ordtrest2lem  19790  cnpco  19854  cncls2  19860  cncnpi  19865  cncnp  19867  cnconst2  19870  cnpdis  19880  lmcnp  19891  cnhaus  19941  isreg2  19964  cncmp  19978  tgcmp  19987  sscmp  19991  cmpfi  19994  cnconn  20008  iunconlem  20013  clscon  20016  1stcfb  20031  1stcrest  20039  2ndcctbss  20041  2ndcdisj  20042  1stcelcls  20047  1stccnp  20048  restnlly  20068  cldllycmp  20081  lly1stc  20082  dislly  20083  locfincmp  20112  comppfsc  20118  kgentopon  20124  kgenidm  20133  1stckgenlem  20139  kgencn3  20144  ptpjpre1  20157  ptbasin  20163  txcls  20190  tx2cn  20196  ptpjcn  20197  ptclsg  20201  ptcnp  20208  txdis  20218  txlly  20222  txnlly  20223  pthaus  20224  txtube  20226  txcmplem1  20227  txcmplem2  20228  txcmp  20229  txhaus  20233  txkgen  20238  xkohaus  20239  xkococnlem  20245  xkococn  20246  txcon  20275  qtopeu  20302  qtoprest  20303  regr1lem2  20326  kqreglem1  20327  cmphaushmeo  20386  xkocnv  20400  fgabs  20465  filuni  20471  trufil  20496  ufileu  20505  filufint  20506  fin1aufil  20518  elfm2  20534  rnelfmlem  20538  fmfnfmlem2  20541  fmfnfmlem4  20543  fmufil  20545  flimopn  20561  fbflim2  20563  hausflimi  20566  hausflim  20567  flimcf  20568  flimclslem  20570  flimsncls  20572  hauspwpwf1  20573  cnpflfi  20585  fclsnei  20605  fclscf  20611  flimfnfcls  20614  fclscmp  20616  ufilcmp  20618  fcfnei  20621  cnpfcf  20627  alexsublem  20629  alexsub  20630  alexsubALTlem2  20633  alexsubALTlem3  20634  alexsubALTlem4  20635  ptcmplem3  20639  ptcmplem4  20640  ptcmplem5  20641  symgtgp  20685  tgpconcompeqg  20695  tgpconcomp  20696  ghmcnp  20698  tgpt0  20702  qustgplem  20704  haustsms2  20720  tsmsgsum  20722  tsmsgsumOLD  20725  tsmsresOLD  20730  tsmsres  20731  tsmsxp  20742  imasdsf1olem  20961  xbln0  21002  blssps  21012  blss  21013  neibl  21089  blcld  21093  metss  21096  metequiv2  21098  met1stc  21109  metrest  21112  prdsxmslem2  21117  metcnp3  21128  nrmmetd  21180  nlmvscnlem1  21280  nrginvrcnlem  21284  nmoleub  21323  icccmplem2  21413  icccmp  21415  reconnlem2  21417  xrge0tsms  21424  metdstri  21440  metdseq0  21443  metdscn  21445  cnmpt2pc  21513  lebnumlem3  21548  pcoval2  21601  pcopt  21607  nmoleub2lem  21682  nmhmcn  21688  ipcnlem1  21770  cfilfcls  21798  cmetcaulem  21812  iscmet3lem2  21816  iscmet3  21817  equivcau  21824  caubl  21831  bcthlem2  21849  bcthlem3  21850  bcthlem4  21851  bcthlem5  21852  ivthlem2  21949  ivthlem3  21950  ovoliunlem2  21999  ovolicc2lem2  22014  ovolicc2lem3  22015  ovolicc2lem5  22017  ovolicc2  22018  ismbl2  22023  nulmbl  22031  nulmbl2  22032  unmbl  22033  shftmbl  22034  voliunlem3  22047  volsup  22051  ioombl1lem4  22056  ioombl1  22057  icombl  22059  ioombl  22060  uniioombl  22083  opnmbllem  22095  volivth  22101  vitali  22107  mbflimsup  22158  i1fadd  22187  itg1addlem4  22191  itg2le  22231  itg2seq  22234  itg2lea  22236  itg2splitlem  22240  itg2split  22241  itg2mono  22245  itg2gt0  22252  itg2cnlem2  22254  itgss  22303  itgfsum  22318  itgcn  22334  ellimc3  22368  limcco  22382  limciun  22383  dvnres  22419  dvnfre  22440  rolle  22476  c1liplem1  22482  dvivth  22496  dvne0  22497  lhop1lem  22499  lhop1  22500  lhop  22502  dvcnvrelem1  22503  dvfsumrlim  22517  dvfsum2  22520  ftc1a  22523  ftc1lem6  22527  itgsubst  22535  tdeglem4  22543  mdegaddle  22559  mdegvscale  22560  mdegmullem  22563  deg1tmle  22603  ply1divex  22622  dvdsq1p  22646  fta1g  22653  fta1b  22655  plyco0  22674  coeeulem  22706  dgrlem  22711  plyco  22723  coemullem  22732  dgreq0  22747  dgrco  22757  plydivex  22778  quotcan  22790  aannenlem1  22809  aalioulem2  22814  aalioulem3  22815  taylthlem1  22853  ulmbdd  22878  itgulm  22888  radcnvlt1  22898  psercnlem1  22905  abelthlem2  22912  abelthlem8  22919  logcnlem5  23114  efopn  23126  cxpmul2z  23159  cxpcn3lem  23208  cxpeq  23218  xrlimcnp  23415  cxplim  23418  o1cxp  23421  cxploglim  23424  scvxcvx  23432  jensen  23435  ftalem1  23463  ftalem2  23464  fta  23470  basellem3  23473  isppw2  23506  ppinprm  23543  chtnprm  23545  dvdsmulf1o  23587  chtublem  23603  perfectlem2  23622  dchrfi  23647  dchrptlem1  23656  dchrptlem2  23657  dchrptlem3  23658  dchrsum2  23660  bposlem1  23676  bposlem3  23678  2sqlem5  23760  2sqlem6  23761  2sqlem8  23764  2sqlem10  23766  2sqb  23770  chebbnd1lem1  23771  chtppilimlem2  23776  dchrisum0flb  23812  dchrisum0fno1  23813  dchrisum0  23822  pntrsumbnd2  23869  pntpbnd1  23888  pntpbnd2  23889  pntlemp  23912  pnt3  23914  qabvle  23927  ostth2lem2  23936  ostth3  23940  ostth  23941  colinearalglem4  24333  axcontlem10  24397  umgraex  24444  eupai  25088  numclwwlkovf2ex  25207  isgrp2d  25354  ghgrpOLD  25487  ghabloOLD  25488  smcnlem  25724  ubthlem1  25903  ubthlem3  25905  htthlem  25951  5oalem6  26694  leopmuli  27168  pjnormssi  27203  pjclem4  27234  pj3si  27242  hatomistici  27397  sumdmdlem  27453  suppss2f  27617  xrge0tsmsd  27929  isarchiofld  27961  ordtrest2NEWlem  28058  qqhf  28120  eulerpartlemb  28490  ballotlemfc0  28614  ballotlemfcc  28615  sgn3da  28663  subfacp1lem5  28817  erdszelem7  28830  erdszelem11  28834  pconcon  28865  txpcon  28866  conpcon  28869  sconpi1  28873  txscon  28875  cvxscon  28877  cvmopnlem  28912  cvmfolem  28913  cvmliftmolem2  28916  cvmliftlem7  28925  cvmliftlem10  28928  cvmlift2lem10  28946  cvmlift3lem4  28956  cvmlift3lem8  28960  msubff1  29105  wzel  29545  wsuclem  29546  nofulllem4  29630  btwnouttr2  29825  cgrxfr  29858  btwnxfr  29859  brcolinear  29862  lineext  29879  btwnconn1lem13  29902  midofsegid  29907  segcon2  29908  brsegle  29911  seglecgr12im  29913  segletr  29917  colinbtwnle  29921  broutsideof2  29925  btwnoutside  29928  broutsideof3  29929  outsideoftr  29932  outsideofeq  29933  outsideofeu  29934  outsidele  29935  lineunray  29950  lineelsb2  29951  linethru  29956  wl-sbcom2d-lem1  30174  finixpnum  30203  supaddc  30206  heicant  30214  opnmbllem0  30215  mblfinlem3  30218  ismblfin  30220  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  itg2addnclem  30232  itg2addnclem3  30234  ftc1cnnc  30255  finminlem  30302  nn0prpwlem  30306  neibastop2lem  30344  neibastop2  30345  neibastop3  30346  topjoin  30349  tailfb  30361  sdclem2  30401  fdc  30404  istotbnd3  30433  isbnd2  30445  isbnd3  30446  prdsbnd  30455  cntotbnd  30458  heibor1lem  30471  heibor1  30472  heiborlem10  30482  rrncmslem  30494  ghomco  30511  1idl  30589  unichnidl  30594  prtlem10  30772  prtlem18  30784  isnacs3  30808  fnwe2lem2  31163  kelac1  31175  hbtlem5  31245  hbt  31247  dgraa0p  31266  hashgcdeq  31326  rlimdmafv  32428  perfectALTVlem2  32544  mgmhmeql  32809  lindslinindsimp2  33264  atlatmstc  35457  cvrexchlem  35556  paddasslem14  35970  pexmidlem5N  36111  cdleme29ex  36513  cdlemefr29exN  36541  cdleme32fva  36576  diarnN  37269  dihlsscpre  37374
  Copyright terms: Public domain W3C validator