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

Theorem expr 599
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 589 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  rexlimdvaa  2831  disjxiun  4209  wereu2  4579  suppss  5863  fcof1  6020  knatar  6080  ovmpt2df  6205  suppss2  6300  riota5f  6574  smoord  6627  tfrlem9a  6647  oaass  6804  oelimcl  6843  oaabs2  6888  swoso  6936  eceqoveq  7009  domdifsn  7191  domunsncan  7208  omxpenlem  7209  mapdom2  7278  frfi  7352  fofinf1o  7387  finsschain  7413  elfiun  7435  marypha1lem  7438  eqsupd  7462  ordiso2  7484  ordtypelem6  7492  ordtypelem7  7493  ordtypelem10  7496  oismo  7509  wemapso2lem  7519  brwdom2  7541  wdomtr  7543  unwdomg  7552  xpwdomg  7553  unxpwdom2  7556  cantnfval2  7624  cantnfle  7626  cantnfreslem  7631  cantnflem1  7645  cantnf  7649  r1ordg  7704  tcrank  7808  carddomi2  7857  harval2  7884  infxpenlem  7895  infxpenc2lem2  7901  fseqenlem1  7905  dfac8clem  7913  acndom2  7935  infpwfien  7943  iunfictbso  7995  dfac12lem3  8025  infxp  8095  coflim  8141  cofsmo  8149  coftr  8153  sornom  8157  infpssrlem4  8186  enfin2i  8201  fin23lem26  8205  fin23lem27  8208  fin23lem36  8228  fin23lem40  8231  isf32lem5  8237  isf34lem4  8257  isfin1-3  8266  fin1a2lem10  8289  fin1a2lem13  8292  fin1a2s  8294  hsmexlem4  8309  ttukeylem5  8393  ttukeylem6  8394  ttukeylem7  8395  alephval2  8447  gchor  8502  fpwwe2lem7  8511  fpwwe2lem12  8516  fpwwe2  8518  pwfseqlem4a  8536  pwfseqlem4  8537  winalim2  8571  gchina  8574  inar1  8650  nqereq  8812  prlem934  8910  prlem936  8924  supsrlem  8986  axpre-sup  9044  prodge0  9857  supmul1  9973  un0addcl  10253  un0mulcl  10254  uzwo3  10569  qbtwnre  10785  xlemul1a  10867  seqcl2  11341  seqfveq2  11345  seqshft2  11349  monoord  11353  seqsplit  11356  seqf1olem1  11362  seqid2  11369  seqhomo  11370  expnegz  11414  expcan  11432  ltexp2  11433  discr  11516  bcval5  11609  hashbc  11702  hashf1lem2  11705  seqcoll  11712  seqcoll2  11713  wrdind  11791  cau3lem  12158  ello1d  12317  lo1bdd2  12318  rlimclim  12340  climrlim2  12341  rlimdm  12345  rlimcn1  12382  reccn2  12390  rlimsqzlem  12442  lo1le  12445  caucvgrlem  12466  caurcvg2  12471  summolem2  12510  zsum  12512  fsum  12514  fsumf1o  12517  sumss  12518  fsumss  12519  fsumcl2lem  12525  fsumadd  12532  fsumcom2  12558  fsum0diag2  12566  fsummulc2  12567  fsumconst  12573  fsumrelem  12586  fsumrlim  12590  fsumo1  12591  divrcnv  12632  geomulcvg  12653  mertenslem2  12662  ruclem8  12836  dvds0lem  12860  dvdsnegb  12867  dvdssub2  12887  bitsf1  12958  bitsshft  12987  bezoutlem3  13040  bezoutlem4  13041  isprm2lem  13086  isprm6  13109  isprm5  13112  pcqmul  13227  pcqcl  13230  pcxcl  13234  pc2dvds  13252  pcadd  13258  pcmpt  13261  pockthg  13274  infpnlem1  13278  prmreclem5  13288  vdwlem2  13350  vdwlem9  13357  vdwlem10  13358  vdwlem12  13360  ramub  13381  0ram  13388  ramub1lem2  13395  ramub1  13396  ramcl  13397  mreexexd  13873  acsfn2  13888  iscatd  13898  catpropd  13935  setcmon  14242  drsdirfi  14395  pleval2i  14421  psss  14646  mhmeql  14764  gsumvallem1  14771  frmdss2  14808  frmdup3  14811  grprcan  14838  mulgnn0ass  14919  isnsg3  14974  ghmpreima  15027  ghmeql  15028  gaorber  15085  oddvds  15185  gexdvds  15218  sylow1lem1  15232  odcau  15238  pgpssslw  15248  sylow2alem2  15252  sylow2blem3  15256  fislw  15259  sylow2  15260  lsmmod  15307  efgredlem  15379  frgpup3  15410  gexex  15468  gsumval3  15514  gsumzres  15517  gsumzcl  15518  gsumzf1o  15519  gsumzaddlem  15526  gsumconst  15532  gsumzmhm  15533  gsumzoppg  15539  gsum2d2lem  15547  ablfac1eulem  15630  pgpfac1lem5  15637  ablfaclem3  15645  issubdrg  15893  lss1d  16039  lmhmeql  16131  lspextmo  16132  lspsnat  16217  lsppratlem6  16224  islbs3  16227  lbsextlem4  16233  lidl1el  16289  mvrf1  16489  mplsubglem  16498  mpllsslem  16499  mplcoe1  16528  mplcoe2  16530  cnsubrg  16759  gsumfsum  16766  prmirredlem  16773  znidomb  16842  frgpcyg  16854  cssmre  16920  en2top  17050  toponmre  17157  topssnei  17188  innei  17189  clslp  17212  restcls  17245  restntr  17246  ordtrest2lem  17267  cnpco  17331  cncls2  17337  cncnpi  17342  cncnp  17344  cnconst2  17347  cnpdis  17357  lmcnp  17368  cnhaus  17418  nrmsep  17421  regsep2  17440  isreg2  17441  cncmp  17455  tgcmp  17464  sscmp  17468  cmpfi  17471  cnconn  17485  iunconlem  17490  clscon  17493  1stcfb  17508  1stcrest  17516  2ndcctbss  17518  2ndcdisj  17519  1stcelcls  17524  1stccnp  17525  restnlly  17545  cldllycmp  17558  lly1stc  17559  dislly  17560  kgentopon  17570  kgenidm  17579  1stckgenlem  17585  kgencn3  17590  ptpjpre1  17603  ptbasin  17609  txcls  17636  tx2cn  17642  ptpjcn  17643  ptclsg  17647  ptcnp  17654  txdis  17664  txlly  17668  txnlly  17669  pthaus  17670  txtube  17672  txcmplem1  17673  txcmplem2  17674  txcmp  17675  txhaus  17679  txkgen  17684  xkohaus  17685  xkococnlem  17691  xkococn  17692  txcon  17721  qtopeu  17748  qtoprest  17749  regr1lem2  17772  kqreglem1  17773  cmphaushmeo  17832  xkocnv  17846  fgabs  17911  filuni  17917  trufil  17942  ufileu  17951  filufint  17952  fin1aufil  17964  elfm2  17980  rnelfmlem  17984  fmfnfmlem2  17987  fmfnfmlem4  17989  fmufil  17991  flimopn  18007  fbflim2  18009  hausflimi  18012  hausflim  18013  flimcf  18014  flimclslem  18016  flimsncls  18018  hauspwpwf1  18019  cnpflfi  18031  fclsnei  18051  fclscf  18057  flimfnfcls  18060  fclscmp  18062  ufilcmp  18064  fcfnei  18067  cnpfcf  18073  alexsublem  18075  alexsub  18076  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  ptcmplem3  18085  ptcmplem4  18086  ptcmplem5  18087  symgtgp  18131  tgpconcompeqg  18141  tgpconcomp  18142  ghmcnp  18144  tgpt0  18148  divstgplem  18150  haustsms2  18166  tsmsgsum  18168  tsmsres  18173  tsmsxp  18184  imasdsf1olem  18403  xbln0  18444  blssps  18454  blss  18455  neibl  18531  blcld  18535  metss  18538  metequiv2  18540  met1stc  18551  metrest  18554  prdsxmslem2  18559  metcnp3  18570  nrmmetd  18622  nlmvscnlem1  18722  nrginvrcnlem  18726  nmoleub  18765  icccmplem2  18854  icccmp  18856  reconnlem2  18858  xrge0tsms  18865  metdstri  18881  metdseq0  18884  metdscn  18886  cnmpt2pc  18953  cnheibor  18980  lebnumlem3  18988  pcoval2  19041  pcopt  19047  nmoleub2lem  19122  nmhmcn  19128  ipcnlem1  19199  cfilfcls  19227  cmetcaulem  19241  iscmet3lem2  19245  iscmet3  19246  equivcau  19253  caubl  19260  lmcau  19265  bcthlem2  19278  bcthlem3  19279  bcthlem4  19280  bcthlem5  19281  ivthlem2  19349  ivthlem3  19350  ovoliunlem2  19399  ovolicc2lem2  19414  ovolicc2lem3  19415  ovolicc2lem5  19417  ovolicc2  19418  ismbl2  19423  nulmbl  19430  nulmbl2  19431  unmbl  19432  shftmbl  19433  voliunlem3  19446  volsup  19450  ioombl1lem4  19455  ioombl1  19456  icombl  19458  ioombl  19459  uniioombl  19481  opnmbllem  19493  volivth  19499  vitali  19505  ismbf3d  19546  mbflimsup  19558  i1fadd  19587  itg1addlem4  19591  itg2le  19631  itg2seq  19634  itg2lea  19636  itg2splitlem  19640  itg2split  19641  itg2mono  19645  itg2gt0  19652  itg2cnlem2  19654  itgss  19703  itgfsum  19718  itgcn  19734  ellimc3  19766  limcco  19780  limciun  19781  dvnres  19817  dvnfre  19838  rolle  19874  c1liplem1  19880  dvivth  19894  dvne0  19895  lhop1lem  19897  lhop1  19898  lhop  19900  dvcnvrelem1  19901  dvfsumrlim  19915  dvfsum2  19918  ftc1a  19921  ftc1lem6  19925  itgsubst  19933  tdeglem4  19983  mdegaddle  19997  mdegvscale  19998  mdegmullem  20001  deg1tmle  20040  ply1divex  20059  dvdsq1p  20083  fta1g  20090  fta1b  20092  plyco0  20111  coeeulem  20143  dgrlem  20148  plyco  20160  coemullem  20168  dgreq0  20183  dgrco  20193  plydivex  20214  quotcan  20226  aannenlem1  20245  aalioulem2  20250  aalioulem3  20251  taylthlem1  20289  ulmbdd  20314  ulmdvlem3  20318  itgulm  20324  radcnvlt1  20334  psercnlem1  20341  abelthlem2  20348  abelthlem8  20355  logcnlem5  20537  efopn  20549  cxpmul2z  20582  cxpcn3lem  20631  cxpeq  20641  xrlimcnp  20807  cxplim  20810  o1cxp  20813  cxploglim  20816  scvxcvx  20824  jensen  20827  ftalem1  20855  ftalem2  20856  fta  20862  basellem3  20865  isppw2  20898  ppinprm  20935  chtnprm  20937  dvdsmulf1o  20979  chtublem  20995  perfectlem2  21014  dchrfi  21039  dchrptlem1  21048  dchrptlem2  21049  dchrptlem3  21050  dchrsum2  21052  bposlem1  21068  bposlem3  21070  2sqlem5  21152  2sqlem6  21153  2sqlem8  21156  2sqlem10  21158  2sqb  21162  chebbnd1lem1  21163  chtppilimlem2  21168  dchrisum0flb  21204  dchrisum0fno1  21205  dchrisum0  21214  pntrsumbnd2  21261  pntpbnd1  21280  pntpbnd2  21281  pntlemp  21304  pnt3  21306  qabvle  21319  ostth2lem2  21328  ostth3  21332  ostth  21333  umgraex  21358  eupai  21689  isgrp2d  21823  ghgrp  21956  ghablo  21957  smcnlem  22193  ubthlem1  22372  ubthlem3  22374  htthlem  22420  pjhthlem2  22894  5oalem6  23161  leopmuli  23636  pjnormssi  23671  pjclem4  23702  pj3si  23710  hatomistici  23865  sumdmdlem  23921  reximddv  23962  suppss2f  24049  xrge0tsmsd  24223  qqhf  24370  ballotlemfc0  24750  ballotlemfcc  24751  subfacp1lem5  24870  erdszelem7  24883  erdszelem11  24887  pconcon  24918  txpcon  24919  conpcon  24922  sconpi1  24926  txscon  24928  cvxscon  24930  cvmopnlem  24965  cvmfolem  24966  cvmliftmolem2  24969  cvmliftlem7  24978  cvmliftlem10  24981  cvmliftlem15  24985  cvmlift2lem10  24999  cvmlift3lem4  25009  cvmlift3lem8  25013  dedekind  25187  dedekindle  25188  mulge0b  25191  prodmolem2  25261  zprod  25263  fprod  25267  fprodf1o  25272  prodss  25273  fprodss  25274  fprodcl2lem  25276  fprodmul  25284  fproddiv  25285  fprodconst  25302  fprodn0  25303  fprodcom2  25308  wzel  25575  wsuclem  25576  nofulllem4  25660  colinearalglem4  25848  axcontlem10  25912  btwnouttr2  25956  cgrxfr  25989  btwnxfr  25990  brcolinear  25993  lineext  26010  btwnconn1lem13  26033  midofsegid  26038  segcon2  26039  brsegle  26042  seglecgr12im  26044  segletr  26048  colinbtwnle  26052  broutsideof2  26056  btwnoutside  26059  broutsideof3  26060  outsideoftr  26063  outsideofeq  26064  outsideofeu  26065  outsidele  26066  lineunray  26081  lineelsb2  26082  linethru  26087  supaddc  26237  opnmbllem0  26242  mblfinlem3  26245  ismblfin  26247  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  itg2addnclem  26256  itg2addnclem3  26258  ftc1cnnc  26279  finminlem  26321  nn0prpwlem  26325  locfincmp  26384  comppfsc  26387  neibastop2lem  26389  neibastop2  26390  neibastop3  26391  topjoin  26394  tailfb  26406  sdclem2  26446  fdc  26449  istotbnd3  26480  isbnd2  26492  isbnd3  26493  prdsbnd  26502  cntotbnd  26505  heibor1lem  26518  heibor1  26519  heiborlem10  26529  rrncmslem  26541  ghomco  26558  1idl  26636  unichnidl  26641  prtlem10  26714  prtlem18  26726  isnacs3  26764  nacsfix  26766  fnwe2lem2  27126  kelac1  27138  dsmmsubg  27186  dsmmlss  27187  frlmsslsp  27225  unxpwdom3  27233  enfixsn  27234  lindff1  27267  lindfrn  27268  hbtlem5  27309  hbt  27311  dgraa0p  27331  f1omvdco2  27368  psgnunilem1  27393  psgnunilem2  27395  hashgcdeq  27494  rlimdmafv  28017  modprminv  28225  modprminveq  28226  reumodprminv  28227  cshwidx  28242  atlatmstc  30117  cvrexchlem  30216  paddasslem14  30630  pexmidlem5N  30771  cdleme29ex  31171  cdlemefr29exN  31199  cdleme32fva  31234  diarnN  31927  dihlsscpre  32032
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 178  df-an 361
  Copyright terms: Public domain W3C validator