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  2835  rexlimdvaa  2852  disjxiun  4358  wereu2  4788  fcof1  6139  knatar  6202  riota5f  6230  ovmpt2df  6381  extmptsuppeq  6889  suppss  6895  suppss2  6899  wfrlem17  7002  smoord  7034  tfrlem9a  7054  oaass  7212  oelimcl  7251  oaabs2  7296  swoso  7344  eceqoveq  7418  domdifsn  7603  domunsncan  7620  omxpenlem  7621  enfixsn  7629  mapdom2  7691  frfi  7764  fofinf1o  7800  finsschain  7829  elfiun  7892  marypha1lem  7895  eqsupd  7919  eqinfd  7949  ordiso2  7978  ordtypelem6  7986  ordtypelem7  7987  ordtypelem10  7990  oismo  8003  wemapsolem  8013  brwdom2  8036  wdomtr  8038  unwdomg  8047  xpwdomg  8048  unxpwdom2  8051  cantnfval2  8121  cantnfle  8123  cantnflem1  8141  cantnf  8145  r1ordg  8196  tcrank  8302  carddomi2  8351  harval2  8378  infxpenlem  8391  infxpenc2lem2  8397  fseqenlem1  8401  dfac8clem  8409  acndom2  8431  infpwfien  8439  iunfictbso  8491  dfac12lem3  8521  infxp  8591  coflim  8637  cofsmo  8645  coftr  8649  sornom  8653  infpssrlem4  8682  enfin2i  8697  fin23lem26  8701  fin23lem27  8704  fin23lem36  8724  fin23lem40  8727  isf32lem5  8733  isf34lem4  8753  isfin1-3  8762  fin1a2lem10  8785  fin1a2lem13  8788  fin1a2s  8790  hsmexlem4  8805  ttukeylem5  8889  ttukeylem6  8890  ttukeylem7  8891  alephval2  8943  gchor  8998  fpwwe2lem7  9007  fpwwe2lem12  9012  fpwwe2  9014  pwfseqlem4a  9032  pwfseqlem4  9033  winalim2  9067  gchina  9070  inar1  9146  nqereq  9306  prlem934  9404  prlem936  9418  addsrmo  9443  mulsrmo  9444  supsrlem  9481  axpre-sup  9539  dedekind  9743  dedekindle  9744  prodge0  10398  mulge0b  10421  supaddc  10520  supmul1  10522  un0addcl  10849  un0mulcl  10850  uzwo3  11205  qbtwnre  11438  xlemul1a  11520  seqcl2  12176  seqfveq2  12180  seqshft2  12184  monoord  12188  seqsplit  12191  seqf1olem1  12197  seqid2  12204  seqhomo  12205  expnegz  12251  expcan  12270  ltexp2  12271  discr  12354  bcval5  12448  hashbc  12559  hashf1lem2  12562  seqcoll  12570  seqcoll2  12571  wrdind  12774  wrd2ind  12775  cau3lem  13356  ello1d  13525  lo1bdd2  13526  rlimclim  13548  climrlim2  13549  rlimdm  13553  rlimcn1  13590  reccn2  13598  rlimsqzlem  13650  lo1le  13653  caucvgrlem  13674  caucvgrlemOLD  13675  caurcvg2  13682  summolem2  13720  zsum  13722  fsum  13724  fsumf1o  13727  sumss  13728  fsumss  13729  fsumcl2lem  13735  fsumadd  13743  fsumcom2  13773  fsum0diag2  13782  fsummulc2  13783  fsumconst  13789  fsumrelem  13805  fsumrlim  13809  fsumo1  13810  divrcnv  13848  geomulcvg  13870  mertenslem2  13879  prodmolem2  13927  zprod  13929  fprod  13933  fprodf1o  13938  prodss  13939  fprodss  13940  fprodcl2lem  13942  fprodmul  13952  fproddiv  13953  fprodconst  13970  fprodn0  13971  fprodcom2  13976  ruclem8  14227  dvds0lem  14251  dvdsnegb  14258  dvdssub2  14280  bitsf1  14358  bitsshft  14387  bezoutlem3OLD  14443  bezoutlem4OLD  14444  bezoutlem3  14446  bezoutlem4  14447  isprm2lem  14569  isprm5  14589  isprm6  14604  modprminv  14688  modprminveq  14689  reumodprminv  14693  pcqmul  14741  pcqcl  14744  pcxcl  14748  pc2dvds  14766  pcadd  14772  pcmpt  14775  pockthg  14788  infpnlem1  14792  prmreclem5  14802  vdwlem2  14870  vdwlem9  14877  vdwlem10  14878  vdwlem12  14880  ramub  14908  0ram  14916  ramub1lem2  14923  ramub1  14924  ramcl  14925  mreexexd  15492  acsfn2  15507  iscatd  15517  catpropd  15552  setcmon  15920  pleval2i  16148  psss  16398  mgmidsssn0  16450  mhmeql  16549  frmdss2  16585  frmdup3  16589  grprcan  16637  mulgnn0ass  16725  isnsg3  16789  ghmpreima  16842  ghmeql  16843  gaorber  16900  f1omvdco2  17027  psgnunilem1  17072  psgnunilem2  17074  oddvds  17134  gexdvds  17173  sylow1lem1  17188  odcau  17194  pgpssslw  17204  sylow2alem2  17208  sylow2blem3  17212  fislw  17215  lsmmod  17263  efgredlem  17335  frgpup3  17366  gsumval3  17479  gsumzres  17481  gsumzcl2  17482  gsumzf1o  17484  gsumzaddlem  17492  gsumconst  17505  gsumzmhm  17508  gsumzoppg  17515  gsum2d2lem  17543  ablfac1eulem  17643  pgpfac1lem5  17650  ablfaclem3  17658  issubdrg  17971  lss1d  18124  lmhmeql  18216  lspextmo  18217  lspsnat  18306  lsppratlem6  18313  islbs3  18316  lbsextlem4  18322  lidl1el  18380  mvrf1  18587  mplsubglem  18596  mpllsslem  18597  mplcoe1  18627  mplcoe5  18630  gsummoncoe1  18836  cnsubrg  18966  gsumfsum  18972  prmirredlem  19001  znidomb  19069  frgpcyg  19081  cssmre  19193  dsmmsubg  19243  dsmmlss  19244  frlmsslsp  19291  lindff1  19315  lindfrn  19316  mat1dimcrng  19439  mdetdiaglem  19560  mdetunilem7  19580  mdetunilem8  19581  mdetunilem9  19582  cpmatacl  19677  cpmatmcllem  19679  mp2pm2mplem4  19770  en2top  19938  toponmre  20046  topssnei  20077  innei  20078  clslp  20101  restcls  20134  restntr  20135  ordtrest2lem  20156  cnpco  20220  cncls2  20226  cncnpi  20231  cncnp  20233  cnconst2  20236  cnpdis  20246  lmcnp  20257  cnhaus  20307  isreg2  20330  cncmp  20344  tgcmp  20353  sscmp  20357  cmpfi  20360  cnconn  20374  iunconlem  20379  clscon  20382  1stcfb  20397  1stcrest  20405  2ndcctbss  20407  2ndcdisj  20408  1stcelcls  20413  1stccnp  20414  restnlly  20434  cldllycmp  20447  lly1stc  20448  dislly  20449  locfincmp  20478  comppfsc  20484  kgentopon  20490  kgenidm  20499  1stckgenlem  20505  kgencn3  20510  ptpjpre1  20523  ptbasin  20529  txcls  20556  tx2cn  20562  ptpjcn  20563  ptclsg  20567  ptcnp  20574  txdis  20584  txlly  20588  txnlly  20589  pthaus  20590  txtube  20592  txcmplem1  20593  txcmplem2  20594  txcmp  20595  txhaus  20599  txkgen  20604  xkohaus  20605  xkococnlem  20611  xkococn  20612  txcon  20641  qtopeu  20668  qtoprest  20669  regr1lem2  20692  kqreglem1  20693  cmphaushmeo  20752  xkocnv  20766  fgabs  20831  filuni  20837  trufil  20862  ufileu  20871  filufint  20872  fin1aufil  20884  elfm2  20900  rnelfmlem  20904  fmfnfmlem2  20907  fmfnfmlem4  20909  fmufil  20911  flimopn  20927  fbflim2  20929  hausflimi  20932  hausflim  20933  flimcf  20934  flimclslem  20936  flimsncls  20938  hauspwpwf1  20939  cnpflfi  20951  fclsnei  20971  fclscf  20977  flimfnfcls  20980  fclscmp  20982  ufilcmp  20984  fcfnei  20987  cnpfcf  20993  alexsublem  20996  alexsub  20997  alexsubALTlem2  21000  alexsubALTlem3  21001  alexsubALTlem4  21002  ptcmplem3  21006  ptcmplem4  21007  ptcmplem5  21008  symgtgp  21053  tgpconcompeqg  21063  tgpconcomp  21064  ghmcnp  21066  tgpt0  21070  qustgplem  21072  haustsms2  21088  tsmsgsum  21090  tsmsres  21095  tsmsxp  21106  imasdsf1olem  21325  xbln0  21366  blssps  21376  blss  21377  neibl  21453  blcld  21457  metss  21460  metequiv2  21462  met1stc  21473  metrest  21476  prdsxmslem2  21481  metcnp3  21492  nrmmetd  21526  nlmvscnlem1  21626  nrginvrcnlem  21630  nmoleub  21673  nmoleubOLD  21689  icccmplem2  21778  icccmp  21780  reconnlem2  21782  xrge0tsms  21789  metdstri  21805  metdseq0  21808  metdscn  21810  metdstriOLD  21820  metdseq0OLD  21823  metdscnOLD  21825  cnmpt2pc  21893  lebnumlem3  21928  lebnumlem3OLD  21931  pcoval2  21984  pcopt  21990  nmoleub2lem  22065  nmhmcn  22071  ipcnlem1  22153  cfilfcls  22181  cmetcaulem  22195  iscmet3lem2  22199  iscmet3  22200  equivcau  22207  caubl  22214  bcthlem2  22230  bcthlem3  22231  bcthlem4  22232  bcthlem5  22233  ivthlem2  22340  ivthlem3  22341  ovoliunlem2  22393  ovolicc2lem2  22408  ovolicc2lem3  22409  ovolicc2lem5  22412  ovolicc2  22413  ismbl2  22418  nulmbl  22426  nulmbl2  22427  unmbl  22428  shftmbl  22429  voliunlem3  22442  volsup  22446  ioombl1lem4  22451  ioombl1  22452  icombl  22454  ioombl  22455  uniioombl  22484  opnmbllem  22496  volivth  22502  vitali  22508  mbflimsup  22560  mbflimsupOLD  22561  i1fadd  22590  itg1addlem4  22594  itg2le  22634  itg2seq  22637  itg2lea  22639  itg2splitlem  22643  itg2split  22644  itg2mono  22648  itg2gt0  22655  itg2cnlem2  22657  itgss  22706  itgfsum  22721  itgcn  22737  ellimc3  22771  limcco  22785  limciun  22786  dvnres  22822  dvnfre  22843  rolle  22879  c1liplem1  22885  dvivth  22899  dvne0  22900  lhop1lem  22902  lhop1  22903  lhop  22905  dvcnvrelem1  22906  dvfsumrlim  22920  dvfsum2  22923  ftc1a  22926  ftc1lem6  22930  itgsubst  22938  tdeglem4  22946  mdegaddle  22960  mdegvscale  22961  mdegmullem  22964  deg1tmle  23003  ply1divex  23024  dvdsq1p  23048  fta1g  23055  fta1b  23057  plyco0  23083  coeeulem  23115  dgrlem  23120  plyco  23132  coemullem  23141  dgreq0  23156  dgrco  23166  plydivex  23187  quotcan  23199  aannenlem1  23221  aalioulem2  23226  aalioulem3  23227  taylthlem1  23265  ulmbdd  23290  itgulm  23300  radcnvlt1  23310  psercnlem1  23317  abelthlem2  23324  abelthlem8  23331  logcnlem5  23528  efopn  23540  cxpmul2z  23573  cxpcn3lem  23624  cxpeq  23634  xrlimcnp  23831  cxplim  23834  o1cxp  23837  cxploglim  23840  scvxcvx  23848  jensen  23851  ftalem1  23934  ftalem2  23935  fta  23943  basellem3  23946  isppw2  23979  ppinprm  24016  chtnprm  24018  dvdsmulf1o  24060  chtublem  24076  perfectlem2  24095  dchrfi  24120  dchrptlem1  24129  dchrptlem2  24130  dchrptlem3  24131  dchrsum2  24133  bposlem1  24149  bposlem3  24151  2sqlem5  24233  2sqlem6  24234  2sqlem8  24237  2sqlem10  24239  2sqb  24243  chebbnd1lem1  24244  chtppilimlem2  24249  dchrisum0flb  24285  dchrisum0fno1  24286  dchrisum0  24295  pntrsumbnd2  24342  pntpbnd1  24361  pntpbnd2  24362  pntlemp  24385  pnt3  24387  qabvle  24400  ostth2lem2  24409  ostth3  24413  ostth  24414  colinearalglem4  24876  axcontlem10  24940  umgraex  24987  eupai  25632  numclwwlkovf2ex  25751  isgrp2d  25900  ghgrpOLD  26033  ghabloOLD  26034  smcnlem  26270  ubthlem1  26449  ubthlem3  26451  htthlem  26507  5oalem6  27249  leopmuli  27723  pjnormssi  27758  pjclem4  27789  pj3si  27797  hatomistici  27952  sumdmdlem  28008  suppss2fOLD  28178  xrge0tsmsd  28495  isarchiofld  28527  ordtrest2NEWlem  28675  qqhf  28737  eulerpartlemb  29148  ballotlemfc0  29272  ballotlemfcc  29273  sgn3da  29359  subfacp1lem5  29854  erdszelem7  29867  erdszelem11  29871  pconcon  29901  txpcon  29902  conpcon  29905  sconpi1  29909  txscon  29911  cvxscon  29913  cvmopnlem  29948  cvmfolem  29949  cvmliftmolem2  29952  cvmliftlem7  29961  cvmliftlem10  29964  cvmlift2lem10  29982  cvmlift3lem4  29992  cvmlift3lem8  29996  msubff1  30141  wzel  30453  wsuclem  30454  nofulllem4  30538  btwnouttr2  30733  cgrxfr  30766  btwnxfr  30767  brcolinear  30770  lineext  30787  btwnconn1lem13  30810  midofsegid  30815  segcon2  30816  brsegle  30819  seglecgr12im  30821  segletr  30825  colinbtwnle  30829  broutsideof2  30833  btwnoutside  30836  broutsideof3  30837  outsideoftr  30840  outsideofeq  30841  outsideofeu  30842  outsidele  30843  lineunray  30858  lineelsb2  30859  linethru  30864  finminlem  30918  nn0prpwlem  30922  neibastop2lem  30960  neibastop2  30961  neibastop3  30962  topjoin  30965  tailfb  30977  relowlssretop  31673  wl-sbcom2d-lem1  31796  finixpnum  31837  poimirlem6  31853  poimirlem7  31854  poimirlem13  31860  poimirlem26  31873  poimirlem29  31876  heicant  31882  opnmbllem0  31883  mblfinlem3  31886  ismblfin  31888  ovoliunnfl  31889  voliunnfl  31891  volsupnfl  31892  itg2addnclem  31900  itg2addnclem3  31902  ftc1cnnc  31923  sdclem2  31978  fdc  31981  istotbnd3  32010  isbnd2  32022  isbnd3  32023  prdsbnd  32032  cntotbnd  32035  heibor1lem  32048  heibor1  32049  heiborlem10  32059  rrncmslem  32071  ghomco  32088  1idl  32166  unichnidl  32171  prtlem10  32348  prtlem18  32360  atlatmstc  32797  cvrexchlem  32896  paddasslem14  33310  pexmidlem5N  33451  cdleme29ex  33853  cdlemefr29exN  33881  cdleme32fva  33916  diarnN  34609  dihlsscpre  34714  isnacs3  35464  fnwe2lem2  35822  kelac1  35834  hbtlem5  35900  hbt  35902  dgraa0p  35928  hashgcdeq  35988  rlimdmafv  38492  smonoord  38531  perfectALTVlem2  38657  upgrex  38958  mgmhmeql  39394  lindslinindsimp2  39849
  Copyright terms: Public domain W3C validator