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

Theorem expr 615
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 605 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 429 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  reximddv  2939  rexlimdvaa  2956  disjxiun  4444  wereu2  4876  suppssOLD  6012  fcof1  6176  knatar  6239  riota5f  6268  ovmpt2df  6416  suppss2OLD  6512  extmptsuppeq  6921  suppss  6927  suppss2  6931  smoord  7033  tfrlem9a  7052  oaass  7207  oelimcl  7246  oaabs2  7291  swoso  7339  eceqoveq  7413  domdifsn  7597  domunsncan  7614  omxpenlem  7615  enfixsn  7623  mapdom2  7685  frfi  7761  fofinf1o  7797  finsschain  7823  elfiun  7886  marypha1lem  7889  eqsupd  7913  ordiso2  7936  ordtypelem6  7944  ordtypelem7  7945  ordtypelem10  7948  oismo  7961  wemapsolem  7971  brwdom2  7995  wdomtr  7997  unwdomg  8006  xpwdomg  8007  unxpwdom2  8010  cantnfval2  8084  cantnfle  8086  cantnflem1  8104  cantnf  8108  cantnfval2OLD  8114  cantnfleOLD  8116  cantnflem1OLD  8127  cantnfOLD  8130  r1ordg  8192  tcrank  8298  carddomi2  8347  harval2  8374  infxpenlem  8387  infxpenc2lem2  8393  infxpenc2lem2OLD  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  9001  fpwwe2lem7  9010  fpwwe2lem12  9015  fpwwe2  9017  pwfseqlem4a  9035  pwfseqlem4  9036  winalim2  9070  gchina  9073  inar1  9149  nqereq  9309  prlem934  9407  prlem936  9421  addsrmo  9446  mulsrmo  9447  supsrlem  9484  axpre-sup  9542  dedekind  9739  dedekindle  9740  prodge0  10385  mulge0b  10408  supmul1  10504  un0addcl  10825  un0mulcl  10826  uzwo3  11173  qbtwnre  11394  xlemul1a  11476  seqcl2  12088  seqfveq2  12092  seqshft2  12096  monoord  12100  seqsplit  12103  seqf1olem1  12109  seqid2  12116  seqhomo  12117  expnegz  12162  expcan  12180  ltexp2  12181  discr  12265  bcval5  12358  hashbc  12462  hashf1lem2  12465  seqcoll  12472  seqcoll2  12473  wrdind  12659  wrd2ind  12660  cau3lem  13143  ello1d  13302  lo1bdd2  13303  rlimclim  13325  climrlim2  13326  rlimdm  13330  rlimcn1  13367  reccn2  13375  rlimsqzlem  13427  lo1le  13430  caucvgrlem  13451  caurcvg2  13456  summolem2  13494  zsum  13496  fsum  13498  fsumf1o  13501  sumss  13502  fsumss  13503  fsumcl2lem  13509  fsumadd  13517  fsumcom2  13545  fsum0diag2  13554  fsummulc2  13555  fsumconst  13561  fsumrelem  13577  fsumrlim  13581  fsumo1  13582  divrcnv  13620  geomulcvg  13641  mertenslem2  13650  ruclem8  13824  dvds0lem  13848  dvdsnegb  13855  dvdssub2  13875  bitsf1  13948  bitsshft  13977  bezoutlem3  14030  bezoutlem4  14031  isprm2lem  14076  isprm6  14102  isprm5  14105  modprminv  14178  modprminveq  14179  reumodprminv  14181  pcqmul  14229  pcqcl  14232  pcxcl  14236  pc2dvds  14254  pcadd  14260  pcmpt  14263  pockthg  14276  infpnlem1  14280  prmreclem5  14290  vdwlem2  14352  vdwlem9  14359  vdwlem10  14360  vdwlem12  14362  ramub  14383  0ram  14390  ramub1lem2  14397  ramub1  14398  ramcl  14399  mreexexd  14896  acsfn2  14911  iscatd  14921  catpropd  14958  setcmon  15265  drsdirfi  15418  pleval2i  15444  psss  15694  mhmeql  15802  gsumvallem1  15810  frmdss2  15851  frmdup3  15854  grprcan  15881  mulgnn0ass  15968  isnsg3  16027  ghmpreima  16080  ghmeql  16081  gaorber  16138  f1omvdco2  16266  psgnunilem1  16311  psgnunilem2  16313  oddvds  16364  gexdvds  16397  sylow1lem1  16411  odcau  16417  pgpssslw  16427  sylow2alem2  16431  sylow2blem3  16435  fislw  16438  sylow2  16439  lsmmod  16486  efgredlem  16558  frgpup3  16589  gexex  16649  gsumval3OLD  16696  gsumval3  16699  gsumzres  16702  gsumzcl2  16703  gsumzf1o  16705  gsumzresOLD  16706  gsumzclOLD  16707  gsumzf1oOLD  16708  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumconst  16742  gsumzmhm  16745  gsumzmhmOLD  16746  gsumzoppg  16755  gsumzoppgOLD  16756  gsum2d2lem  16789  ablfac1eulem  16910  pgpfac1lem5  16917  ablfaclem3  16925  issubdrg  17234  lss1d  17389  lmhmeql  17481  lspextmo  17482  lspsnat  17571  lsppratlem6  17578  islbs3  17581  lbsextlem4  17587  lidl1el  17645  mvrf1  17849  mplsubglem  17861  mpllsslem  17862  mplsubglemOLD  17863  mpllsslemOLD  17864  mplcoe1  17895  mplcoe5  17899  mplcoe2OLD  17901  gsummoncoe1  18114  cnsubrg  18243  gsumfsum  18249  prmirredlem  18287  prmirredlemOLD  18290  znidomb  18364  frgpcyg  18376  cssmre  18488  dsmmsubg  18538  dsmmlss  18539  frlmsslsp  18593  frlmsslspOLD  18594  lindff1  18619  lindfrn  18620  mat1dimcrng  18743  mdetdiaglem  18864  mdetunilem7  18884  mdetunilem8  18885  mdetunilem9  18886  cpmatacl  18981  cpmatmcllem  18983  mp2pm2mplem4  19074  en2top  19250  toponmre  19357  topssnei  19388  innei  19389  clslp  19412  restcls  19445  restntr  19446  ordtrest2lem  19467  cnpco  19531  cncls2  19537  cncnpi  19542  cncnp  19544  cnconst2  19547  cnpdis  19557  lmcnp  19568  cnhaus  19618  nrmsep  19621  regsep2  19640  isreg2  19641  cncmp  19655  tgcmp  19664  sscmp  19668  cmpfi  19671  cnconn  19686  iunconlem  19691  clscon  19694  1stcfb  19709  1stcrest  19717  2ndcctbss  19719  2ndcdisj  19720  1stcelcls  19725  1stccnp  19726  restnlly  19746  cldllycmp  19759  lly1stc  19760  dislly  19761  kgentopon  19771  kgenidm  19780  1stckgenlem  19786  kgencn3  19791  ptpjpre1  19804  ptbasin  19810  txcls  19837  tx2cn  19843  ptpjcn  19844  ptclsg  19848  ptcnp  19855  txdis  19865  txlly  19869  txnlly  19870  pthaus  19871  txtube  19873  txcmplem1  19874  txcmplem2  19875  txcmp  19876  txhaus  19880  txkgen  19885  xkohaus  19886  xkococnlem  19892  xkococn  19893  txcon  19922  qtopeu  19949  qtoprest  19950  regr1lem2  19973  kqreglem1  19974  cmphaushmeo  20033  xkocnv  20047  fgabs  20112  filuni  20118  trufil  20143  ufileu  20152  filufint  20153  fin1aufil  20165  elfm2  20181  rnelfmlem  20185  fmfnfmlem2  20188  fmfnfmlem4  20190  fmufil  20192  flimopn  20208  fbflim2  20210  hausflimi  20213  hausflim  20214  flimcf  20215  flimclslem  20217  flimsncls  20219  hauspwpwf1  20220  cnpflfi  20232  fclsnei  20252  fclscf  20258  flimfnfcls  20261  fclscmp  20263  ufilcmp  20265  fcfnei  20268  cnpfcf  20274  alexsublem  20276  alexsub  20277  alexsubALTlem2  20280  alexsubALTlem3  20281  alexsubALTlem4  20282  ptcmplem3  20286  ptcmplem4  20287  ptcmplem5  20288  symgtgp  20332  tgpconcompeqg  20342  tgpconcomp  20343  ghmcnp  20345  tgpt0  20349  divstgplem  20351  haustsms2  20367  tsmsgsum  20369  tsmsgsumOLD  20372  tsmsresOLD  20377  tsmsres  20378  tsmsxp  20389  imasdsf1olem  20608  xbln0  20649  blssps  20659  blss  20660  neibl  20736  blcld  20740  metss  20743  metequiv2  20745  met1stc  20756  metrest  20759  prdsxmslem2  20764  metcnp3  20775  nrmmetd  20827  nlmvscnlem1  20927  nrginvrcnlem  20931  nmoleub  20970  icccmplem2  21060  icccmp  21062  reconnlem2  21064  xrge0tsms  21071  metdstri  21087  metdseq0  21090  metdscn  21092  cnmpt2pc  21160  cnheibor  21187  lebnumlem3  21195  pcoval2  21248  pcopt  21254  nmoleub2lem  21329  nmhmcn  21335  ipcnlem1  21417  cfilfcls  21445  cmetcaulem  21459  iscmet3lem2  21463  iscmet3  21464  equivcau  21471  caubl  21478  lmcau  21483  bcthlem2  21496  bcthlem3  21497  bcthlem4  21498  bcthlem5  21499  ivthlem2  21596  ivthlem3  21597  ovoliunlem2  21646  ovolicc2lem2  21661  ovolicc2lem3  21662  ovolicc2lem5  21664  ovolicc2  21665  ismbl2  21670  nulmbl  21678  nulmbl2  21679  unmbl  21680  shftmbl  21681  voliunlem3  21694  volsup  21698  ioombl1lem4  21703  ioombl1  21704  icombl  21706  ioombl  21707  uniioombl  21730  opnmbllem  21742  volivth  21748  vitali  21754  ismbf3d  21793  mbflimsup  21805  i1fadd  21834  itg1addlem4  21838  itg2le  21878  itg2seq  21881  itg2lea  21883  itg2splitlem  21887  itg2split  21888  itg2mono  21892  itg2gt0  21899  itg2cnlem2  21901  itgss  21950  itgfsum  21965  itgcn  21981  ellimc3  22015  limcco  22029  limciun  22030  dvnres  22066  dvnfre  22087  rolle  22123  c1liplem1  22129  dvivth  22143  dvne0  22144  lhop1lem  22146  lhop1  22147  lhop  22149  dvcnvrelem1  22150  dvfsumrlim  22164  dvfsum2  22167  ftc1a  22170  ftc1lem6  22174  itgsubst  22182  tdeglem4  22190  mdegaddle  22206  mdegvscale  22207  mdegmullem  22210  deg1tmle  22250  ply1divex  22269  dvdsq1p  22293  fta1g  22300  fta1b  22302  plyco0  22321  coeeulem  22353  dgrlem  22358  plyco  22370  coemullem  22378  dgreq0  22393  dgrco  22403  plydivex  22424  quotcan  22436  aannenlem1  22455  aalioulem2  22460  aalioulem3  22461  taylthlem1  22499  ulmbdd  22524  ulmdvlem3  22528  itgulm  22534  radcnvlt1  22544  psercnlem1  22551  abelthlem2  22558  abelthlem8  22565  logcnlem5  22752  efopn  22764  cxpmul2z  22797  cxpcn3lem  22846  cxpeq  22856  xrlimcnp  23023  cxplim  23026  o1cxp  23029  cxploglim  23032  scvxcvx  23040  jensen  23043  ftalem1  23071  ftalem2  23072  fta  23078  basellem3  23081  isppw2  23114  ppinprm  23151  chtnprm  23153  dvdsmulf1o  23195  chtublem  23211  perfectlem2  23230  dchrfi  23255  dchrptlem1  23264  dchrptlem2  23265  dchrptlem3  23266  dchrsum2  23268  bposlem1  23284  bposlem3  23286  2sqlem5  23368  2sqlem6  23369  2sqlem8  23372  2sqlem10  23374  2sqb  23378  chebbnd1lem1  23379  chtppilimlem2  23384  dchrisum0flb  23420  dchrisum0fno1  23421  dchrisum0  23430  pntrsumbnd2  23477  pntpbnd1  23496  pntpbnd2  23497  pntlemp  23520  pnt3  23522  qabvle  23535  ostth2lem2  23544  ostth3  23548  ostth  23549  colinearalglem4  23885  axcontlem10  23949  umgraex  23996  eupai  24640  numclwwlkovf2ex  24760  isgrp2d  24910  ghgrp  25043  ghablo  25044  smcnlem  25280  ubthlem1  25459  ubthlem3  25461  htthlem  25507  pjhthlem2  25983  5oalem6  26250  leopmuli  26725  pjnormssi  26760  pjclem4  26791  pj3si  26799  hatomistici  26954  sumdmdlem  27010  suppss2f  27147  xrge0tsmsd  27435  isarchiofld  27467  ordtrest2NEWlem  27537  qqhf  27600  eulerpartlemb  27944  ballotlemfc0  28068  ballotlemfcc  28069  sgn3da  28117  subfacp1lem5  28265  erdszelem7  28278  erdszelem11  28282  pconcon  28313  txpcon  28314  conpcon  28317  sconpi1  28321  txscon  28323  cvxscon  28325  cvmopnlem  28360  cvmfolem  28361  cvmliftmolem2  28364  cvmliftlem7  28373  cvmliftlem10  28376  cvmliftlem15  28380  cvmlift2lem10  28394  cvmlift3lem4  28404  cvmlift3lem8  28408  prodmolem2  28641  zprod  28643  fprod  28647  fprodf1o  28652  prodss  28653  fprodss  28654  fprodcl2lem  28656  fprodmul  28664  fproddiv  28665  fprodconst  28682  fprodn0  28683  fprodcom2  28688  wzel  28954  wsuclem  28955  nofulllem4  29039  btwnouttr2  29246  cgrxfr  29279  btwnxfr  29280  brcolinear  29283  lineext  29300  btwnconn1lem13  29323  midofsegid  29328  segcon2  29329  brsegle  29332  seglecgr12im  29334  segletr  29338  colinbtwnle  29342  broutsideof2  29346  btwnoutside  29349  broutsideof3  29350  outsideoftr  29353  outsideofeq  29354  outsideofeu  29355  outsidele  29356  lineunray  29371  lineelsb2  29372  linethru  29377  wl-sbcom2d-lem1  29583  finixpnum  29612  supaddc  29615  heicant  29624  opnmbllem0  29625  mblfinlem3  29628  ismblfin  29630  ovoliunnfl  29631  voliunnfl  29633  volsupnfl  29634  itg2addnclem  29641  itg2addnclem3  29643  ftc1cnnc  29664  finminlem  29711  nn0prpwlem  29715  locfincmp  29774  comppfsc  29777  neibastop2lem  29779  neibastop2  29780  neibastop3  29781  topjoin  29784  tailfb  29796  sdclem2  29836  fdc  29839  istotbnd3  29868  isbnd2  29880  isbnd3  29881  prdsbnd  29890  cntotbnd  29893  heibor1lem  29906  heibor1  29907  heiborlem10  29917  rrncmslem  29929  ghomco  29946  1idl  30024  unichnidl  30029  prtlem10  30208  prtlem18  30220  isnacs3  30244  nacsfix  30246  fnwe2lem2  30601  kelac1  30613  unxpwdom3  30645  hbtlem5  30681  hbt  30683  dgraa0p  30703  hashgcdeq  30763  rlimdmafv  31729  lindslinindsimp2  32137  atlatmstc  34116  cvrexchlem  34215  paddasslem14  34629  pexmidlem5N  34770  cdleme29ex  35170  cdlemefr29exN  35198  cdleme32fva  35233  diarnN  35926  dihlsscpre  36031
  Copyright terms: Public domain W3C validator