MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expr 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  2799  disjxiun  4177  wereu2  4547  suppss  5830  fcof1  5987  knatar  6047  ovmpt2df  6172  suppss2  6267  riota5f  6541  smoord  6594  tfrlem9a  6614  oaass  6771  oelimcl  6810  oaabs2  6855  swoso  6903  eceqoveq  6976  domdifsn  7158  domunsncan  7175  omxpenlem  7176  mapdom2  7245  frfi  7319  fofinf1o  7354  finsschain  7379  elfiun  7401  marypha1lem  7404  eqsupd  7426  ordiso2  7448  ordtypelem6  7456  ordtypelem7  7457  ordtypelem10  7460  oismo  7473  wemapso2lem  7483  brwdom2  7505  wdomtr  7507  unwdomg  7516  xpwdomg  7517  unxpwdom2  7520  cantnfval2  7588  cantnfle  7590  cantnfreslem  7595  cantnflem1  7609  cantnf  7613  r1ordg  7668  tcrank  7772  carddomi2  7821  harval2  7848  infxpenlem  7859  infxpenc2lem2  7865  fseqenlem1  7869  dfac8clem  7877  acndom2  7899  infpwfien  7907  iunfictbso  7959  dfac12lem3  7989  infxp  8059  coflim  8105  cofsmo  8113  coftr  8117  sornom  8121  infpssrlem4  8150  enfin2i  8165  fin23lem26  8169  fin23lem27  8172  fin23lem36  8192  fin23lem40  8195  isf32lem5  8201  isf34lem4  8221  isfin1-3  8230  fin1a2lem10  8253  fin1a2lem13  8256  fin1a2s  8258  hsmexlem4  8273  ttukeylem5  8357  ttukeylem6  8358  ttukeylem7  8359  alephval2  8411  gchor  8466  fpwwe2lem7  8475  fpwwe2lem12  8480  fpwwe2  8482  pwfseqlem4a  8500  pwfseqlem4  8501  winalim2  8535  gchina  8538  inar1  8614  nqereq  8776  prlem934  8874  prlem936  8888  supsrlem  8950  axpre-sup  9008  prodge0  9821  supmul1  9937  un0addcl  10217  un0mulcl  10218  uzwo3  10533  qbtwnre  10749  xlemul1a  10831  seqcl2  11304  seqfveq2  11308  seqshft2  11312  monoord  11316  seqsplit  11319  seqf1olem1  11325  seqid2  11332  seqhomo  11333  expnegz  11377  expcan  11395  ltexp2  11396  discr  11479  bcval5  11572  hashbc  11665  hashf1lem2  11668  seqcoll  11675  seqcoll2  11676  wrdind  11754  cau3lem  12121  ello1d  12280  lo1bdd2  12281  rlimclim  12303  climrlim2  12304  rlimdm  12308  rlimcn1  12345  reccn2  12353  rlimsqzlem  12405  lo1le  12408  caucvgrlem  12429  caurcvg2  12434  summolem2  12473  zsum  12475  fsum  12477  fsumf1o  12480  sumss  12481  fsumss  12482  fsumcl2lem  12488  fsumadd  12495  fsumcom2  12521  fsum0diag2  12529  fsummulc2  12530  fsumconst  12536  fsumrelem  12549  fsumrlim  12553  fsumo1  12554  divrcnv  12595  geomulcvg  12616  mertenslem2  12625  ruclem8  12799  dvds0lem  12823  dvdsnegb  12830  dvdssub2  12850  bitsf1  12921  bitsshft  12950  bezoutlem3  13003  bezoutlem4  13004  isprm2lem  13049  isprm6  13072  isprm5  13075  pcqmul  13190  pcqcl  13193  pcxcl  13197  pc2dvds  13215  pcadd  13221  pcmpt  13224  pockthg  13237  infpnlem1  13241  prmreclem5  13251  vdwlem2  13313  vdwlem9  13320  vdwlem10  13321  vdwlem12  13323  ramub  13344  0ram  13351  ramub1lem2  13358  ramub1  13359  ramcl  13360  mreexexd  13836  acsfn2  13851  iscatd  13861  catpropd  13898  setcmon  14205  drsdirfi  14358  pleval2i  14384  psss  14609  mhmeql  14727  gsumvallem1  14734  frmdss2  14771  frmdup3  14774  grprcan  14801  mulgnn0ass  14882  isnsg3  14937  ghmpreima  14990  ghmeql  14991  gaorber  15048  oddvds  15148  gexdvds  15181  sylow1lem1  15195  odcau  15201  pgpssslw  15211  sylow2alem2  15215  sylow2blem3  15219  fislw  15222  sylow2  15223  lsmmod  15270  efgredlem  15342  frgpup3  15373  gexex  15431  gsumval3  15477  gsumzres  15480  gsumzcl  15481  gsumzf1o  15482  gsumzaddlem  15489  gsumconst  15495  gsumzmhm  15496  gsumzoppg  15502  gsum2d2lem  15510  ablfac1eulem  15593  pgpfac1lem5  15600  ablfaclem3  15608  issubdrg  15856  lss1d  16002  lmhmeql  16094  lspextmo  16095  lspsnat  16180  lsppratlem6  16187  islbs3  16190  lbsextlem4  16196  lidl1el  16252  mvrf1  16452  mplsubglem  16461  mpllsslem  16462  mplcoe1  16491  mplcoe2  16493  cnsubrg  16722  gsumfsum  16729  prmirredlem  16736  znidomb  16805  frgpcyg  16817  cssmre  16883  en2top  17013  toponmre  17120  topssnei  17151  innei  17152  clslp  17174  restcls  17207  restntr  17208  ordtrest2lem  17229  cnpco  17293  cncls2  17299  cncnpi  17304  cncnp  17306  cnconst2  17309  cnpdis  17319  lmcnp  17330  cnhaus  17380  nrmsep  17383  regsep2  17402  isreg2  17403  cncmp  17417  tgcmp  17426  sscmp  17430  cmpfi  17433  cnconn  17446  iunconlem  17451  clscon  17454  1stcfb  17469  1stcrest  17477  2ndcctbss  17479  2ndcdisj  17480  1stcelcls  17485  1stccnp  17486  restnlly  17506  cldllycmp  17519  lly1stc  17520  dislly  17521  kgentopon  17531  kgenidm  17540  1stckgenlem  17546  kgencn3  17551  ptpjpre1  17564  ptbasin  17570  txcls  17597  tx2cn  17603  ptpjcn  17604  ptclsg  17608  ptcnp  17615  txdis  17625  txlly  17629  txnlly  17630  pthaus  17631  txtube  17633  txcmplem1  17634  txcmplem2  17635  txcmp  17636  txhaus  17640  txkgen  17645  xkohaus  17646  xkococnlem  17652  xkococn  17653  txcon  17682  qtopeu  17709  qtoprest  17710  regr1lem2  17733  kqreglem1  17734  cmphaushmeo  17793  xkocnv  17807  fgabs  17872  filuni  17878  trufil  17903  ufileu  17912  filufint  17913  fin1aufil  17925  elfm2  17941  rnelfmlem  17945  fmfnfmlem2  17948  fmfnfmlem4  17950  fmufil  17952  flimopn  17968  fbflim2  17970  hausflimi  17973  hausflim  17974  flimcf  17975  flimclslem  17977  flimsncls  17979  hauspwpwf1  17980  cnpflfi  17992  fclsnei  18012  fclscf  18018  flimfnfcls  18021  fclscmp  18023  ufilcmp  18025  fcfnei  18028  cnpfcf  18034  alexsublem  18036  alexsub  18037  alexsubALTlem2  18040  alexsubALTlem3  18041  alexsubALTlem4  18042  ptcmplem3  18046  ptcmplem4  18047  ptcmplem5  18048  symgtgp  18092  tgpconcompeqg  18102  tgpconcomp  18103  ghmcnp  18105  tgpt0  18109  divstgplem  18111  haustsms2  18127  tsmsgsum  18129  tsmsres  18134  tsmsxp  18145  imasdsf1olem  18364  xbln0  18405  blssps  18415  blss  18416  neibl  18492  blcld  18496  metss  18499  metequiv2  18501  met1stc  18512  metrest  18515  prdsxmslem2  18520  metcnp3  18531  nrmmetd  18583  nlmvscnlem1  18683  nrginvrcnlem  18687  nmoleub  18726  icccmplem2  18815  icccmp  18817  reconnlem2  18819  xrge0tsms  18826  metdstri  18842  metdseq0  18845  metdscn  18847  cnmpt2pc  18914  cnheibor  18941  lebnumlem3  18949  pcoval2  19002  pcopt  19008  nmoleub2lem  19083  nmhmcn  19089  ipcnlem1  19160  cfilfcls  19188  cmetcaulem  19202  iscmet3lem2  19206  iscmet3  19207  equivcau  19214  caubl  19221  lmcau  19226  bcthlem2  19239  bcthlem3  19240  bcthlem4  19241  bcthlem5  19242  ivthlem2  19310  ivthlem3  19311  ovoliunlem2  19360  ovolicc2lem2  19375  ovolicc2lem3  19376  ovolicc2lem5  19378  ovolicc2  19379  ismbl2  19384  nulmbl  19391  nulmbl2  19392  unmbl  19393  shftmbl  19394  voliunlem3  19407  volsup  19411  ioombl1lem4  19416  ioombl1  19417  icombl  19419  ioombl  19420  uniioombl  19442  opnmbllem  19454  volivth  19460  vitali  19466  ismbf3d  19507  mbflimsup  19519  i1fadd  19548  itg1addlem4  19552  itg2le  19592  itg2seq  19595  itg2lea  19597  itg2splitlem  19601  itg2split  19602  itg2mono  19606  itg2gt0  19613  itg2cnlem2  19615  itgss  19664  itgfsum  19679  itgcn  19695  ellimc3  19727  limcco  19741  limciun  19742  dvnres  19778  dvnfre  19799  rolle  19835  c1liplem1  19841  dvivth  19855  dvne0  19856  lhop1lem  19858  lhop1  19859  lhop  19861  dvcnvrelem1  19862  dvfsumrlim  19876  dvfsum2  19879  ftc1a  19882  ftc1lem6  19886  itgsubst  19894  tdeglem4  19944  mdegaddle  19958  mdegvscale  19959  mdegmullem  19962  deg1tmle  20001  ply1divex  20020  dvdsq1p  20044  fta1g  20051  fta1b  20053  plyco0  20072  coeeulem  20104  dgrlem  20109  plyco  20121  coemullem  20129  dgreq0  20144  dgrco  20154  plydivex  20175  quotcan  20187  aannenlem1  20206  aalioulem2  20211  aalioulem3  20212  taylthlem1  20250  ulmbdd  20275  ulmdvlem3  20279  itgulm  20285  radcnvlt1  20295  psercnlem1  20302  abelthlem2  20309  abelthlem8  20316  logcnlem5  20498  efopn  20510  cxpmul2z  20543  cxpcn3lem  20592  cxpeq  20602  xrlimcnp  20768  cxplim  20771  o1cxp  20774  cxploglim  20777  scvxcvx  20785  jensen  20788  ftalem1  20816  ftalem2  20817  fta  20823  basellem3  20826  isppw2  20859  ppinprm  20896  chtnprm  20898  dvdsmulf1o  20940  chtublem  20956  perfectlem2  20975  dchrfi  21000  dchrptlem1  21009  dchrptlem2  21010  dchrptlem3  21011  dchrsum2  21013  bposlem1  21029  bposlem3  21031  2sqlem5  21113  2sqlem6  21114  2sqlem8  21117  2sqlem10  21119  2sqb  21123  chebbnd1lem1  21124  chtppilimlem2  21129  dchrisum0flb  21165  dchrisum0fno1  21166  dchrisum0  21175  pntrsumbnd2  21222  pntpbnd1  21241  pntpbnd2  21242  pntlemp  21265  pnt3  21267  qabvle  21280  ostth2lem2  21289  ostth3  21293  ostth  21294  umgraex  21319  eupai  21650  isgrp2d  21784  ghgrp  21917  ghablo  21918  smcnlem  22154  ubthlem1  22333  ubthlem3  22335  htthlem  22381  pjhthlem2  22855  5oalem6  23122  leopmuli  23597  pjnormssi  23632  pjclem4  23663  pj3si  23671  hatomistici  23826  sumdmdlem  23882  reximddv  23923  suppss2f  24010  xrge0tsmsd  24184  qqhf  24331  ballotlemfc0  24711  ballotlemfcc  24712  subfacp1lem5  24831  erdszelem7  24844  erdszelem11  24848  pconcon  24879  txpcon  24880  conpcon  24883  sconpi1  24887  txscon  24889  cvxscon  24891  cvmopnlem  24926  cvmfolem  24927  cvmliftmolem2  24930  cvmliftlem7  24939  cvmliftlem10  24942  cvmliftlem15  24946  cvmlift2lem10  24960  cvmlift3lem4  24970  cvmlift3lem8  24974  dedekind  25148  dedekindle  25149  mulge0b  25152  prodmolem2  25222  zprod  25224  fprod  25228  fprodf1o  25233  prodss  25234  fprodss  25235  fprodcl2lem  25237  fprodmul  25245  fproddiv  25246  fprodconst  25263  fprodn0  25264  fprodcom2  25269  nofulllem4  25581  colinearalglem4  25760  axcontlem10  25824  btwnouttr2  25868  cgrxfr  25901  btwnxfr  25902  brcolinear  25905  lineext  25922  btwnconn1lem13  25945  midofsegid  25950  segcon2  25951  brsegle  25954  seglecgr12im  25956  segletr  25960  colinbtwnle  25964  broutsideof2  25968  btwnoutside  25971  broutsideof3  25972  outsideoftr  25975  outsideofeq  25976  outsideofeu  25977  outsidele  25978  lineunray  25993  lineelsb2  25994  linethru  25999  supaddc  26145  mblfinlem  26151  mblfinlem2  26152  ismblfin  26154  ovoliunnfl  26155  voliunnfl  26157  volsupnfl  26158  itg2addnclem  26163  itg2addnclem3  26165  ftc1cnnc  26186  finminlem  26219  nn0prpwlem  26223  locfincmp  26282  comppfsc  26285  neibastop2lem  26287  neibastop2  26288  neibastop3  26289  topjoin  26292  tailfb  26304  sdclem2  26344  fdc  26347  istotbnd3  26378  isbnd2  26390  isbnd3  26391  prdsbnd  26400  cntotbnd  26403  heibor1lem  26416  heibor1  26417  heiborlem10  26427  rrncmslem  26439  ghomco  26456  1idl  26534  unichnidl  26539  prtlem10  26612  prtlem18  26624  isnacs3  26662  nacsfix  26664  fnwe2lem2  27024  kelac1  27037  dsmmsubg  27085  dsmmlss  27086  frlmsslsp  27124  unxpwdom3  27132  enfixsn  27133  lindff1  27166  lindfrn  27167  hbtlem5  27208  hbt  27210  dgraa0p  27230  f1omvdco2  27267  psgnunilem1  27292  psgnunilem2  27294  hashgcdeq  27393  rlimdmafv  27916  atlatmstc  29814  cvrexchlem  29913  paddasslem14  30327  pexmidlem5N  30468  cdleme29ex  30868  cdlemefr29exN  30896  cdleme32fva  30931  diarnN  31624  dihlsscpre  31729
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