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

Theorem expr 624
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 614 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 435 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  reximddv  2875  rexlimdvaa  2892  disjxiun  4413  wereu2  4850  fcof1  6210  knatar  6273  riota5f  6301  ovmpt2df  6455  extmptsuppeq  6966  suppss  6972  suppss2  6976  wfrlem17  7078  smoord  7110  tfrlem9a  7130  oaass  7288  oelimcl  7327  oaabs2  7372  swoso  7420  eceqoveq  7494  domdifsn  7681  domunsncan  7698  omxpenlem  7699  enfixsn  7707  mapdom2  7769  frfi  7842  fofinf1o  7878  finsschain  7907  elfiun  7970  marypha1lem  7973  eqsupd  7997  eqinfd  8027  ordiso2  8056  ordtypelem6  8064  ordtypelem7  8065  ordtypelem10  8068  oismo  8081  wemapsolem  8091  brwdom2  8114  wdomtr  8116  unwdomg  8125  xpwdomg  8126  unxpwdom2  8129  cantnfval2  8200  cantnfle  8202  cantnflem1  8220  cantnf  8224  r1ordg  8275  tcrank  8381  carddomi2  8430  harval2  8457  infxpenlem  8470  infxpenc2lem2  8477  fseqenlem1  8481  dfac8clem  8489  acndom2  8511  infpwfien  8519  iunfictbso  8571  dfac12lem3  8601  infxp  8671  coflim  8717  cofsmo  8725  coftr  8729  sornom  8733  infpssrlem4  8762  enfin2i  8777  fin23lem26  8781  fin23lem27  8784  fin23lem36  8804  fin23lem40  8807  isf32lem5  8813  isf34lem4  8833  isfin1-3  8842  fin1a2lem10  8865  fin1a2lem13  8868  fin1a2s  8870  hsmexlem4  8885  ttukeylem5  8969  ttukeylem6  8970  ttukeylem7  8971  alephval2  9023  gchor  9078  fpwwe2lem7  9087  fpwwe2lem12  9092  fpwwe2  9094  pwfseqlem4a  9112  pwfseqlem4  9113  winalim2  9147  gchina  9150  inar1  9226  nqereq  9386  prlem934  9484  prlem936  9498  addsrmo  9523  mulsrmo  9524  supsrlem  9561  axpre-sup  9619  dedekind  9823  dedekindle  9824  prodge0  10480  mulge0b  10503  supaddc  10602  supmul1  10604  un0addcl  10932  un0mulcl  10933  uzwo3  11288  qbtwnre  11521  xlemul1a  11603  seqcl2  12263  seqfveq2  12267  seqshft2  12271  monoord  12275  seqsplit  12278  seqf1olem1  12284  seqid2  12291  seqhomo  12292  expnegz  12338  expcan  12357  ltexp2  12358  discr  12441  bcval5  12535  hashbc  12649  hashf1lem2  12652  seqcoll  12660  seqcoll2  12661  wrdind  12870  wrd2ind  12871  cau3lem  13466  ello1d  13636  lo1bdd2  13637  rlimclim  13659  climrlim2  13660  rlimdm  13664  rlimcn1  13701  reccn2  13709  rlimsqzlem  13761  lo1le  13764  caucvgrlem  13785  caucvgrlemOLD  13786  caurcvg2  13793  summolem2  13831  zsum  13833  fsum  13835  fsumf1o  13838  sumss  13839  fsumss  13840  fsumcl2lem  13846  fsumadd  13854  fsumcom2  13884  fsum0diag2  13893  fsummulc2  13894  fsumconst  13900  fsumrelem  13916  fsumrlim  13920  fsumo1  13921  divrcnv  13959  geomulcvg  13981  mertenslem2  13990  prodmolem2  14038  zprod  14040  fprod  14044  fprodf1o  14049  prodss  14050  fprodss  14051  fprodcl2lem  14053  fprodmul  14063  fproddiv  14064  fprodconst  14081  fprodn0  14082  fprodcom2  14087  ruclem8  14338  dvds0lem  14362  dvdsnegb  14369  dvdssub2  14391  bitsf1  14469  bitsshft  14498  bezoutlem3OLD  14554  bezoutlem4OLD  14555  bezoutlem3  14557  bezoutlem4  14558  isprm2lem  14680  isprm5  14700  isprm6  14715  modprminv  14799  modprminveq  14800  reumodprminv  14804  pcqmul  14852  pcqcl  14855  pcxcl  14859  pc2dvds  14877  pcadd  14883  pcmpt  14886  pockthg  14899  infpnlem1  14903  prmreclem5  14913  vdwlem2  14981  vdwlem9  14988  vdwlem10  14989  vdwlem12  14991  ramub  15019  0ram  15027  ramub1lem2  15034  ramub1  15035  ramcl  15036  mreexexd  15603  acsfn2  15618  iscatd  15628  catpropd  15663  setcmon  16031  pleval2i  16259  psss  16509  mgmidsssn0  16561  mhmeql  16660  frmdss2  16696  frmdup3  16700  grprcan  16748  mulgnn0ass  16836  isnsg3  16900  ghmpreima  16953  ghmeql  16954  gaorber  17011  f1omvdco2  17138  psgnunilem1  17183  psgnunilem2  17185  oddvds  17245  gexdvds  17284  sylow1lem1  17299  odcau  17305  pgpssslw  17315  sylow2alem2  17319  sylow2blem3  17323  fislw  17326  lsmmod  17374  efgredlem  17446  frgpup3  17477  gsumval3  17590  gsumzres  17592  gsumzcl2  17593  gsumzf1o  17595  gsumzaddlem  17603  gsumconst  17616  gsumzmhm  17619  gsumzoppg  17626  gsum2d2lem  17654  ablfac1eulem  17754  pgpfac1lem5  17761  ablfaclem3  17769  issubdrg  18082  lss1d  18235  lmhmeql  18327  lspextmo  18328  lspsnat  18417  lsppratlem6  18424  islbs3  18427  lbsextlem4  18433  lidl1el  18491  mvrf1  18698  mplsubglem  18707  mpllsslem  18708  mplcoe1  18738  mplcoe5  18741  gsummoncoe1  18947  cnsubrg  19077  gsumfsum  19083  prmirredlem  19113  znidomb  19181  frgpcyg  19193  cssmre  19305  dsmmsubg  19355  dsmmlss  19356  frlmsslsp  19403  lindff1  19427  lindfrn  19428  mat1dimcrng  19551  mdetdiaglem  19672  mdetunilem7  19692  mdetunilem8  19693  mdetunilem9  19694  cpmatacl  19789  cpmatmcllem  19791  mp2pm2mplem4  19882  en2top  20050  toponmre  20158  topssnei  20189  innei  20190  clslp  20213  restcls  20246  restntr  20247  ordtrest2lem  20268  cnpco  20332  cncls2  20338  cncnpi  20343  cncnp  20345  cnconst2  20348  cnpdis  20358  lmcnp  20369  cnhaus  20419  isreg2  20442  cncmp  20456  tgcmp  20465  sscmp  20469  cmpfi  20472  cnconn  20486  iunconlem  20491  clscon  20494  1stcfb  20509  1stcrest  20517  2ndcctbss  20519  2ndcdisj  20520  1stcelcls  20525  1stccnp  20526  restnlly  20546  cldllycmp  20559  lly1stc  20560  dislly  20561  locfincmp  20590  comppfsc  20596  kgentopon  20602  kgenidm  20611  1stckgenlem  20617  kgencn3  20622  ptpjpre1  20635  ptbasin  20641  txcls  20668  tx2cn  20674  ptpjcn  20675  ptclsg  20679  ptcnp  20686  txdis  20696  txlly  20700  txnlly  20701  pthaus  20702  txtube  20704  txcmplem1  20705  txcmplem2  20706  txcmp  20707  txhaus  20711  txkgen  20716  xkohaus  20717  xkococnlem  20723  xkococn  20724  txcon  20753  qtopeu  20780  qtoprest  20781  regr1lem2  20804  kqreglem1  20805  cmphaushmeo  20864  xkocnv  20878  fgabs  20943  filuni  20949  trufil  20974  ufileu  20983  filufint  20984  fin1aufil  20996  elfm2  21012  rnelfmlem  21016  fmfnfmlem2  21019  fmfnfmlem4  21021  fmufil  21023  flimopn  21039  fbflim2  21041  hausflimi  21044  hausflim  21045  flimcf  21046  flimclslem  21048  flimsncls  21050  hauspwpwf1  21051  cnpflfi  21063  fclsnei  21083  fclscf  21089  flimfnfcls  21092  fclscmp  21094  ufilcmp  21096  fcfnei  21099  cnpfcf  21105  alexsublem  21108  alexsub  21109  alexsubALTlem2  21112  alexsubALTlem3  21113  alexsubALTlem4  21114  ptcmplem3  21118  ptcmplem4  21119  ptcmplem5  21120  symgtgp  21165  tgpconcompeqg  21175  tgpconcomp  21176  ghmcnp  21178  tgpt0  21182  qustgplem  21184  haustsms2  21200  tsmsgsum  21202  tsmsres  21207  tsmsxp  21218  imasdsf1olem  21437  xbln0  21478  blssps  21488  blss  21489  neibl  21565  blcld  21569  metss  21572  metequiv2  21574  met1stc  21585  metrest  21588  prdsxmslem2  21593  metcnp3  21604  nrmmetd  21638  nlmvscnlem1  21738  nrginvrcnlem  21742  nmoleub  21785  nmoleubOLD  21801  icccmplem2  21890  icccmp  21892  reconnlem2  21894  xrge0tsms  21901  metdstri  21917  metdseq0  21920  metdscn  21922  metdstriOLD  21932  metdseq0OLD  21935  metdscnOLD  21937  cnmpt2pc  22005  lebnumlem3  22040  lebnumlem3OLD  22043  pcoval2  22096  pcopt  22102  nmoleub2lem  22177  nmhmcn  22183  ipcnlem1  22265  cfilfcls  22293  cmetcaulem  22307  iscmet3lem2  22311  iscmet3  22312  equivcau  22319  caubl  22326  bcthlem2  22342  bcthlem3  22343  bcthlem4  22344  bcthlem5  22345  ivthlem2  22452  ivthlem3  22453  ovoliunlem2  22505  ovolicc2lem2  22520  ovolicc2lem3  22521  ovolicc2lem5  22524  ovolicc2  22525  ismbl2  22530  nulmbl  22538  nulmbl2  22539  unmbl  22540  shftmbl  22541  voliunlem3  22554  volsup  22558  ioombl1lem4  22563  ioombl1  22564  icombl  22566  ioombl  22567  uniioombl  22596  opnmbllem  22608  volivth  22614  vitali  22620  mbflimsup  22672  mbflimsupOLD  22673  i1fadd  22702  itg1addlem4  22706  itg2le  22746  itg2seq  22749  itg2lea  22751  itg2splitlem  22755  itg2split  22756  itg2mono  22760  itg2gt0  22767  itg2cnlem2  22769  itgss  22818  itgfsum  22833  itgcn  22849  ellimc3  22883  limcco  22897  limciun  22898  dvnres  22934  dvnfre  22955  rolle  22991  c1liplem1  22997  dvivth  23011  dvne0  23012  lhop1lem  23014  lhop1  23015  lhop  23017  dvcnvrelem1  23018  dvfsumrlim  23032  dvfsum2  23035  ftc1a  23038  ftc1lem6  23042  itgsubst  23050  tdeglem4  23058  mdegaddle  23072  mdegvscale  23073  mdegmullem  23076  deg1tmle  23115  ply1divex  23136  dvdsq1p  23160  fta1g  23167  fta1b  23169  plyco0  23195  coeeulem  23227  dgrlem  23232  plyco  23244  coemullem  23253  dgreq0  23268  dgrco  23278  plydivex  23299  quotcan  23311  aannenlem1  23333  aalioulem2  23338  aalioulem3  23339  taylthlem1  23377  ulmbdd  23402  itgulm  23412  radcnvlt1  23422  psercnlem1  23429  abelthlem2  23436  abelthlem8  23443  logcnlem5  23640  efopn  23652  cxpmul2z  23685  cxpcn3lem  23736  cxpeq  23746  xrlimcnp  23943  cxplim  23946  o1cxp  23949  cxploglim  23952  scvxcvx  23960  jensen  23963  ftalem1  24046  ftalem2  24047  fta  24055  basellem3  24058  isppw2  24091  ppinprm  24128  chtnprm  24130  dvdsmulf1o  24172  chtublem  24188  perfectlem2  24207  dchrfi  24232  dchrptlem1  24241  dchrptlem2  24242  dchrptlem3  24243  dchrsum2  24245  bposlem1  24261  bposlem3  24263  2sqlem5  24345  2sqlem6  24346  2sqlem8  24349  2sqlem10  24351  2sqb  24355  chebbnd1lem1  24356  chtppilimlem2  24361  dchrisum0flb  24397  dchrisum0fno1  24398  dchrisum0  24407  pntrsumbnd2  24454  pntpbnd1  24473  pntpbnd2  24474  pntlemp  24497  pnt3  24499  qabvle  24512  ostth2lem2  24521  ostth3  24525  ostth  24526  colinearalglem4  24988  axcontlem10  25052  umgraex  25099  eupai  25744  numclwwlkovf2ex  25863  isgrp2d  26012  ghgrpOLD  26145  ghabloOLD  26146  smcnlem  26382  ubthlem1  26561  ubthlem3  26563  htthlem  26619  5oalem6  27361  leopmuli  27835  pjnormssi  27870  pjclem4  27901  pj3si  27909  hatomistici  28064  sumdmdlem  28120  suppss2fOLD  28286  xrge0tsmsd  28597  isarchiofld  28629  ordtrest2NEWlem  28777  qqhf  28839  eulerpartlemb  29250  ballotlemfc0  29374  ballotlemfcc  29375  sgn3da  29461  subfacp1lem5  29956  erdszelem7  29969  erdszelem11  29973  pconcon  30003  txpcon  30004  conpcon  30007  sconpi1  30011  txscon  30013  cvxscon  30015  cvmopnlem  30050  cvmfolem  30051  cvmliftmolem2  30054  cvmliftlem7  30063  cvmliftlem10  30066  cvmlift2lem10  30084  cvmlift3lem4  30094  cvmlift3lem8  30098  msubff1  30243  wzel  30556  wsuclem  30557  nofulllem4  30643  btwnouttr2  30838  cgrxfr  30871  btwnxfr  30872  brcolinear  30875  lineext  30892  btwnconn1lem13  30915  midofsegid  30920  segcon2  30921  brsegle  30924  seglecgr12im  30926  segletr  30930  colinbtwnle  30934  broutsideof2  30938  btwnoutside  30941  broutsideof3  30942  outsideoftr  30945  outsideofeq  30946  outsideofeu  30947  outsidele  30948  lineunray  30963  lineelsb2  30964  linethru  30969  finminlem  31023  nn0prpwlem  31027  neibastop2lem  31065  neibastop2  31066  neibastop3  31067  topjoin  31070  tailfb  31082  relowlssretop  31811  wl-sbcom2d-lem1  31934  finixpnum  31975  poimirlem6  31991  poimirlem7  31992  poimirlem13  31998  poimirlem26  32011  poimirlem29  32014  heicant  32020  opnmbllem0  32021  mblfinlem3  32024  ismblfin  32026  ovoliunnfl  32027  voliunnfl  32029  volsupnfl  32030  itg2addnclem  32038  itg2addnclem3  32040  ftc1cnnc  32061  sdclem2  32116  fdc  32119  istotbnd3  32148  isbnd2  32160  isbnd3  32161  prdsbnd  32170  cntotbnd  32173  heibor1lem  32186  heibor1  32187  heiborlem10  32197  rrncmslem  32209  ghomco  32226  1idl  32304  unichnidl  32309  prtlem10  32482  prtlem18  32494  atlatmstc  32930  cvrexchlem  33029  paddasslem14  33443  pexmidlem5N  33584  cdleme29ex  33986  cdlemefr29exN  34014  cdleme32fva  34049  diarnN  34742  dihlsscpre  34847  isnacs3  35597  fnwe2lem2  35954  kelac1  35966  hbtlem5  36032  hbt  36034  dgraa0p  36060  hashgcdeq  36120  rlimdmafv  38717  smonoord  38756  perfectALTVlem2  38882  upgrex  39231  mgmhmeql  40076  lindslinindsimp2  40529
  Copyright terms: Public domain W3C validator