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

Theorem expr 598
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 588 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  rexlimdvaa  2668  disjxiun  4020  wereu2  4390  suppss  5658  fcof1  5797  knatar  5857  ovmpt2df  5979  grprinvlem  6058  grpridd  6060  suppss2  6073  riota5f  6329  smoord  6382  tfrlem9a  6402  oaass  6559  oelimcl  6598  nnawordex  6635  oaabs2  6643  swoso  6691  eceqoveq  6763  domdifsn  6945  domunsncan  6962  omxpenlem  6963  mapdom2  7032  frfi  7102  fofinf1o  7137  finsschain  7162  fiin  7175  elfiun  7183  marypha1lem  7186  eqsupd  7208  ordiso2  7230  ordtypelem6  7238  ordtypelem7  7239  ordtypelem10  7242  oismo  7255  wemaplem3  7263  wemapso2lem  7265  brwdom2  7287  wdomtr  7289  unwdomg  7298  xpwdomg  7299  unxpwdom2  7302  cantnfval2  7370  cantnfle  7372  cantnflt  7373  cantnfreslem  7377  oemapvali  7386  cantnflem1  7391  cantnflem4  7394  cantnf  7395  r1ordg  7450  r1pwss  7456  tcrank  7554  carddomi2  7603  harval2  7630  infxpenlem  7641  infxpenc2lem1  7646  infxpenc2lem2  7647  fseqenlem1  7651  fseqenlem2  7652  dfac8clem  7659  acndom2  7681  infpwfien  7689  iunfictbso  7741  dfac12lem3  7771  infxp  7841  coflim  7887  cofsmo  7895  coftr  7899  sornom  7903  infpssrlem4  7932  enfin2i  7947  fin23lem26  7951  fin23lem27  7954  fin23lem36  7974  fin23lem40  7977  isf32lem5  7983  isf34lem4  8003  isfin1-3  8012  fin1a2lem10  8035  fin1a2lem13  8038  fin1a2s  8040  hsmexlem4  8055  ttukeylem5  8140  ttukeylem6  8141  ttukeylem7  8142  alephval2  8194  gchor  8249  fpwwe2lem7  8258  fpwwe2lem12  8263  fpwwe2  8265  pwfseqlem3  8282  pwfseqlem4a  8283  pwfseqlem4  8284  winalim2  8318  gchina  8321  r1wunlim  8359  wunex2  8360  inttsk  8396  inar1  8397  nqereq  8559  prlem934  8657  prlem936  8671  supsrlem  8733  axpre-sup  8791  addcan  8996  addcan2  8997  negeu  9042  mulcand  9401  prodge0  9603  supmul1  9719  un0addcl  9997  un0mulcl  9998  suprzcl  10091  zsupss  10307  uzwo3  10311  qbtwnre  10526  xralrple  10532  xlemul1a  10608  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqf1olem1  11085  seqid2  11092  seqhomo  11093  expnegz  11136  expcan  11154  ltexp2  11155  expmulnbnd  11233  discr  11238  bcval5  11330  hashbc  11391  hashf1lem2  11394  seqcoll  11401  seqcoll2  11402  wrdind  11477  rexanuz  11829  cau3lem  11838  limsupval2  11954  limsupgre  11955  ello1d  11997  lo1bdd2  11998  rlimclim1  12019  rlimclim  12020  climrlim2  12021  rlimdm  12025  rlimcn1  12062  reccn2  12070  rlimsqzlem  12122  lo1le  12125  caucvgrlem  12145  caurcvg2  12150  summolem2  12189  zsum  12191  fsum  12193  fsumf1o  12196  sumss  12197  fsumss  12198  fsumcvg3  12202  fsumcl2lem  12204  fsumadd  12211  fsumcom2  12237  fsum0diag2  12245  fsummulc2  12246  fsumconst  12252  fsumrelem  12265  fsumrlim  12269  fsumo1  12270  divrcnv  12311  geomulcvg  12332  mertenslem2  12341  rpnnen2  12504  ruclem8  12515  dvds0lem  12539  dvdsnegb  12546  dvdssub2  12566  oexpneg  12590  bitsfi  12628  bitsf1  12637  bitsshft  12666  bezoutlem3  12719  bezoutlem4  12720  isprm2lem  12765  prmind2  12769  isprm6  12788  isprm5  12791  pcqmul  12906  pcqcl  12909  pcxcl  12913  pc2dvds  12931  pcprmpw2  12934  pcadd  12937  pcmpt  12940  pockthg  12953  infpnlem1  12957  prmreclem5  12967  vdwlem2  13029  vdwlem6  13033  vdwlem9  13036  vdwlem10  13037  vdwlem12  13039  ramub  13060  0ram  13067  ramub1lem2  13074  ramub1  13075  ramcl  13076  mreexexd  13550  acsfn2  13565  iscatd  13575  catpropd  13612  setcmon  13919  drsdirfi  14072  pleval2i  14098  psss  14323  mhmeql  14441  gsumvallem1  14448  frmdss2  14485  frmdup3  14488  grprcan  14515  mulgnn0ass  14596  isnsg3  14651  ghmpreima  14704  ghmeql  14705  gaorber  14762  oddvds  14862  gexdvds  14895  sylow1lem1  14909  sylow1  14914  odcau  14915  pgpfi  14916  pgpssslw  14925  sylow2alem2  14929  sylow2blem3  14933  slwhash  14935  fislw  14936  sylow2  14937  sylow3lem2  14939  lsmmod  14984  pj1id  15008  efgsfo  15048  efgredlemc  15054  efgredlem  15056  frgpup3  15087  gexex  15145  lt6abl  15181  ghmcyg  15182  gsumval3  15191  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  gsum2d2lem  15224  dmdprdsplitlem  15272  dpjidcl  15293  ablfac1eulem  15307  pgpfac1lem4  15313  pgpfac1lem5  15314  pgpfaclem2  15317  pgpfaclem3  15318  ablfaclem3  15322  unitgrp  15449  irredrmul  15489  issubdrg  15570  lss1d  15720  lmhmeql  15812  lspextmo  15813  lspsolv  15896  lspsnat  15898  lsppratlem6  15905  islbs3  15908  lbsextlem4  15914  lidl1el  15970  mvrf1  16170  mplsubglem  16179  mpllsslem  16180  mplcoe1  16209  mplcoe2  16211  cnsubrg  16432  gsumfsum  16439  prmirredlem  16446  znidomb  16515  znunit  16517  frgpcyg  16527  cssmre  16593  en2top  16723  toponmre  16830  neiint  16841  topssnei  16861  innei  16862  clslp  16879  restbas  16889  restopnb  16906  restcls  16911  restntr  16912  ordtrest2lem  16933  pnfnei  16950  mnfnei  16951  cnpco  16996  cncls2  17002  cncnpi  17007  cncnp  17009  cnconst2  17011  cnpdis  17021  lmcnp  17032  pnrmopn  17071  haust1  17080  cnhaus  17082  nrmsep  17085  regsep2  17104  isreg2  17105  ordthauslem  17111  cncmp  17119  tgcmp  17128  sscmp  17132  cmpfi  17135  cnconn  17148  iunconlem  17153  clscon  17156  t1conperf  17162  1stcfb  17171  1stcrest  17179  2ndcctbss  17181  2ndcdisj  17182  2ndcomap  17184  dis2ndc  17186  1stcelcls  17187  1stccnp  17188  restnlly  17208  islly2  17210  nllyrest  17212  llyidm  17214  nllyidm  17215  hausllycmp  17220  cldllycmp  17221  lly1stc  17222  dislly  17223  kgentopon  17233  kgenidm  17242  llycmpkgen2  17245  1stckgenlem  17248  kgencn3  17253  ptpjpre1  17266  ptbasin  17272  ptbasfi  17276  txcls  17299  tx2cn  17304  ptpjcn  17305  ptclsg  17309  ptcnp  17316  txdis  17326  txlly  17330  txnlly  17331  pthaus  17332  txtube  17334  txcmplem1  17335  txcmplem2  17336  txcmp  17337  txhaus  17341  txkgen  17346  xkohaus  17347  xkococnlem  17353  xkococn  17354  txcon  17383  basqtop  17402  tgqtop  17403  qtopeu  17407  qtoprest  17408  regr1lem  17430  regr1lem2  17431  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  reghmph  17484  nrmhmph  17485  cmphaushmeo  17491  xkocnv  17505  qtophmeo  17508  fbssfi  17532  trfbas2  17538  fgabs  17574  neifil  17575  filuni  17580  trfil2  17582  trfg  17586  trufil  17605  ssufl  17613  ufileu  17614  filufint  17615  fin1aufil  17627  elfm2  17643  rnelfmlem  17647  fmfnfmlem2  17650  fmfnfmlem4  17652  fmufil  17654  ufldom  17657  flimopn  17670  fbflim2  17672  hausflimi  17675  hausflim  17676  flimcf  17677  flimclslem  17679  flimsncls  17681  hauspwpwf1  17682  cnpflfi  17694  fclsnei  17714  fclscf  17720  fclsfnflim  17722  flimfnfcls  17723  fclscmp  17725  uffclsflim  17726  ufilcmp  17727  fcfnei  17730  cnpfcfi  17735  cnpfcf  17736  alexsublem  17738  alexsub  17739  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem3  17748  ptcmplem4  17749  ptcmplem5  17750  symgtgp  17784  tgpconcompeqg  17794  tgpconcomp  17795  ghmcnp  17797  tgpt0  17801  divstgplem  17803  haustsms2  17819  tsmsgsum  17821  tsmsres  17826  tsmsxp  17837  imasdsf1olem  17937  xbln0  17965  blss  17972  blssex  17973  neibl  18047  blcld  18051  metss  18054  metequiv2  18056  met1stc  18067  met2ndci  18068  metrest  18070  prdsxmslem2  18075  metcnp3  18086  metcnpi3  18092  nrmmetd  18097  nlmvscnlem1  18197  nrginvrcnlem  18201  nmoleub  18240  icccmplem1  18327  icccmplem2  18328  icccmplem3  18329  icccmp  18330  reconnlem2  18332  xrge0tsms  18339  metdstri  18355  metdseq0  18358  metdscn  18360  cnmpt2pc  18426  cnheibor  18453  cnllycmp  18454  bndth  18456  lebnumlem1  18459  lebnumlem3  18461  lebnum  18462  pcoval2  18514  pcopt  18520  pi1blem  18537  nmoleub2lem  18595  nmhmcn  18601  ipcnlem1  18672  iscfil3  18699  cfilfcls  18700  cmetcaulem  18714  iscmet3lem2  18718  iscmet3  18719  equivcau  18726  lmle  18727  caubl  18733  lmcau  18738  cmetss  18740  relcmpcmet  18742  bcthlem2  18747  bcthlem3  18748  bcthlem4  18749  bcthlem5  18750  pjthlem2  18802  ivthlem2  18812  ivthlem3  18813  ovoliunlem2  18862  ovolscalem2  18873  ovolicc2lem2  18877  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  ismbl2  18886  nulmbl  18893  nulmbl2  18894  unmbl  18895  shftmbl  18896  voliunlem3  18909  volsup  18913  ioombl1lem4  18918  ioombl1  18919  icombl  18921  ioombl  18922  uniioombllem6  18943  uniioombl  18944  dyadmbllem  18954  opnmbllem  18956  volivth  18962  vitali  18968  ismbf3d  19009  mbfinf  19020  mbflimsup  19021  i1fadd  19050  itg1addlem4  19054  mbfi1fseqlem6  19075  itg2le  19094  itg2const2  19096  itg2seq  19097  itg2lea  19099  itg2splitlem  19103  itg2split  19104  itg2mono  19108  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  itgss  19166  itgfsum  19181  bddmulibl  19193  itgcn  19197  ellimc3  19229  limcflf  19231  limcco  19243  limciun  19244  dvnres  19280  dvnfre  19301  rolle  19337  c1liplem1  19343  dvivth  19357  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcnvre  19366  dvfsumrlim  19378  dvfsum2  19381  ftc1a  19384  ftc1lem6  19388  itgsubst  19396  tdeglem4  19446  mdegaddle  19460  mdegvscale  19461  mdegmullem  19464  deg1tmle  19503  ply1divex  19522  dvdsq1p  19546  fta1g  19553  fta1b  19555  plyco0  19574  coeeulem  19606  dgrlem  19611  plyco  19623  coemullem  19631  dgreq0  19646  dgrco  19656  plydivex  19677  quotcan  19689  aareccl  19706  aannenlem1  19708  aalioulem2  19713  aalioulem3  19714  taylthlem1  19752  ulmbdd  19775  ulmdvlem3  19779  iblulm  19783  itgulm  19784  radcnvlem1  19789  radcnvlt1  19794  psercnlem1  19801  abelthlem2  19808  abelthlem5  19811  abelthlem8  19815  logcnlem5  19993  efopn  20005  cxpmul2z  20038  cxpcn3lem  20087  cxpeq  20097  dcubic  20142  xrlimcnp  20263  cxplim  20266  o1cxp  20269  cxploglim  20272  scvxcvx  20280  jensen  20283  amgm  20285  ftalem1  20310  ftalem2  20311  fta  20317  basellem3  20320  isppw2  20353  ppinprm  20390  chtnprm  20392  dvdsmulf1o  20434  chtublem  20450  perfectlem2  20469  dchrfi  20494  dchrptlem1  20503  dchrptlem2  20504  dchrptlem3  20505  dchrsum2  20507  sumdchr2  20509  bposlem1  20523  bposlem3  20525  lgsne0  20572  lgsqr  20585  lgsquadlem1  20593  2sqlem5  20607  2sqlem6  20608  2sqlem8  20611  2sqlem10  20613  2sqlem11  20614  2sqb  20617  chebbnd1lem1  20618  chtppilimlem2  20623  dchrisum  20641  dchrvmasumif  20652  dchrisum0flb  20659  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem3  20668  dchrisum0  20669  dchrmusum  20673  dchrvmasum  20674  chpdifbnd  20704  pntrsumbnd2  20716  pntrlog2bnd  20733  pntpbnd1  20735  pntpbnd2  20736  pntibndlem3  20741  pntibnd  20742  pntlemi  20753  pntlemp  20759  pntleml  20760  pnt3  20761  qabvle  20774  ostth2lem2  20783  ostth3  20787  ostth  20788  isgrp2d  20902  ghgrp  21035  ghablo  21036  smcnlem  21270  nmobndi  21353  ubthlem1  21449  ubthlem3  21451  htthlem  21497  pjhthlem2  21971  pjspansn  22156  5oalem6  22238  leopmuli  22713  pjnormssi  22748  pjclem4  22779  pj3si  22787  hatomistici  22942  sumdmdlem  22998  reximddv  23028  xmulcand  23104  suppss2f  23201  xrge0tsmsd  23382  subfacp1lem5  23715  erdszelem7  23728  erdszelem11  23732  cnpcon  23761  pconcon  23762  txpcon  23763  conpcon  23766  pconpi1  23768  sconpi1  23770  txscon  23772  cvxscon  23774  cnllyscon  23776  cvmsss2  23805  cvmcov2  23806  cvmopnlem  23809  cvmfolem  23810  cvmliftmolem2  23813  cvmliftlem7  23822  cvmliftlem10  23825  cvmliftlem15  23829  cvmlift2lem10  23843  cvmliftpht  23849  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3lem8  23857  umgraex  23875  eupai  23883  sinccvg  24006  dedekind  24082  dedekindle  24083  mulge0b  24086  nofulllem4  24359  colinearalglem4  24537  axcontlem10  24601  btwnouttr2  24645  cgrxfr  24678  btwnxfr  24679  brcolinear  24682  lineext  24699  btwnconn1lem13  24722  midofsegid  24727  segcon2  24728  brsegle  24731  seglecgr12im  24733  segletr  24737  colinbtwnle  24741  broutsideof2  24745  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  outsideofeq  24753  outsideofeu  24754  outsidele  24755  lineunray  24770  lineelsb2  24771  linethru  24776  intopcoaconc  25541  efilcp  25552  iscnp4  25563  flfnei2  25577  icccon3  25701  finminlem  26231  nn0prpwlem  26238  locfincmp  26304  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  neibastop3  26311  topjoin  26314  tailfb  26326  sdclem2  26452  fdc  26455  istotbnd3  26495  sstotbnd2  26498  sstotbnd  26499  isbndx  26506  isbnd2  26507  isbnd3  26508  ssbnd  26512  totbndbnd  26513  prdsbnd  26517  prdsbnd2  26519  cntotbnd  26520  heibor1lem  26533  heibor1  26534  heiborlem9  26543  heiborlem10  26544  heibor  26545  rrncmslem  26556  ghomco  26573  1idl  26651  unichnidl  26656  prtlem10  26733  prtlem18  26745  elrfi  26769  isnacs3  26785  nacsfix  26787  fnwe2lem2  27148  kelac1  27161  lmhmfgsplit  27184  dsmmsubg  27209  dsmmlss  27210  frlmsslsp  27248  unxpwdom3  27256  enfixsn  27257  lindff1  27290  lindfrn  27291  hbtlem5  27332  hbt  27334  dgraa0p  27354  f1omvdco2  27391  psgnunilem1  27416  psgnunilem2  27418  psgnunilem3  27419  hashgcdeq  27517  atlatmstc  29509  cvrexchlem  29608  paddasslem14  30022  pexmidlem5N  30163  cdleme29ex  30563  cdlemefr29exN  30591  cdleme32fva  30626  diarnN  31319  dihlsscpre  31424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator