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

Theorem anassrs 630
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anassrs.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
anassrs  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem anassrs
StepHypRef Expression
1 anassrs.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 589 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 422 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anass  631  mpanr1  665  pm2.61ddan  768  pm2.61dda  769  anass1rs  783  anabss5  790  anabss7  795  pm2.61da2ne  2646  2ralbida  2705  2rexbidva  2707  pofun  4479  tfindsg2  4800  imainss  5246  eqfnfv2  5787  fnex  5920  f1elima  5968  fliftfun  5993  isores2  6012  f1oiso  6030  ovmpt2dxf  6158  grpridd  6246  sorpssuni  6490  sorpssint  6491  oalim  6735  omlim  6736  oaass  6763  omlimcl  6780  omass  6782  oelim2  6797  oeoa  6799  oeoelem  6800  nnaass  6824  omabs  6849  eroveu  6958  sbthlem4  7179  fimaxg  7313  fisupg  7314  fofinf1o  7346  ordtypelem7  7449  hartogs  7469  card2on  7478  unwdomg  7508  wemapwe  7610  dfac5  7965  cfsmolem  8106  isf32lem2  8190  ttukeylem6  8350  ondomon  8394  alephreg  8413  ltexprlem6  8874  recexsrlem  8934  wloglei  9515  recextlem2  9609  fimaxre  9911  creur  9950  uzind3OLD  10321  uz11  10464  xrmaxeq  10723  xrmineq  10724  xaddf  10766  xaddass  10784  xleadd1a  10788  xlt2add  10795  xmullem  10799  xmulgt0  10818  xmulasslem3  10821  xlemul1a  10823  xadddilem  10829  fzrevral  11086  seqcaopr2  11314  expnlbnd2  11465  faclbnd4lem4  11542  shftlem  11838  01sqrex  12010  cau3lem  12113  limsupbnd2  12232  clim2  12253  clim2c  12254  clim0c  12256  rlimresb  12314  2clim  12321  climabs0  12334  climcn1  12340  climcn2  12341  o1rlimmul  12367  climsqz  12389  climsqz2  12390  rlimsqzlem  12397  lo1le  12400  climsup  12418  caucvgrlem2  12423  iseralt  12433  summolem2  12465  fsum2dlem  12509  cvgcmp  12550  cvgcmpce  12552  climfsum  12554  fsumiun  12555  geomulcvg  12608  mertenslem2  12617  mertens  12618  smu01lem  12952  gcdcllem1  12966  gcdmultiplez  13006  dvdssq  13015  coprmdvds2  13058  pclem  13167  pcge0  13190  pcgcd1  13205  prmpwdvds  13227  1arithlem4  13249  4sqlem18  13285  vdwlem10  13313  vdwlem11  13314  ramval  13331  ramub1lem2  13350  ramcl  13352  imasaddfnlem  13708  imasaddflem  13710  imasvscafn  13717  imasleval  13721  ismon2  13915  isepi2  13922  issubc3  14001  cofucl  14040  setcmon  14197  setcepi  14198  ipodrsfi  14544  ipodrsima  14546  isacs3lem  14547  grpidpropd  14677  mhmpropd  14699  mhmima  14718  gsumccat  14742  grplcan  14812  mulgdirlem  14869  subgmulg  14913  issubg4  14916  subgint  14919  cycsubgcl  14921  ssnmz  14937  gastacl  15041  orbsta  15045  galactghm  15061  cntzsubg  15090  odmulg  15147  odbezout  15149  sylow3lem2  15217  lsmsubm  15242  efgsfo  15326  mulgmhm  15405  mulgghm  15406  gsumval3  15469  gsumcllem  15471  gsumpt  15500  gsum2d  15501  gsum2d2  15503  prdsgsum  15507  subgdmdprd  15547  dprd2d2  15557  ablfac1eu  15586  rngpropd  15650  rnglghm  15666  dvdsrpropd  15756  abvpropd  15885  islmodd  15911  lmodprop2d  15961  lsssubg  15988  lsspropd  16048  islmhm2  16069  lmhmima  16078  lsmelval2  16112  lidlsubg  16241  assapropd  16341  asclpropd  16359  psrass1lem  16397  mplcoe1  16483  mplcoe2  16485  mplind  16517  evlslem2  16523  coe1tmmul2  16623  phlpropd  16841  neips  17132  neindisj  17136  ordtrest2lem  17221  lmbrf  17278  lmss  17316  isreg2  17395  lmmo  17398  hauscmplem  17423  2ndcomap  17474  1stcelcls  17477  restlly  17499  islly2  17500  cldllycmp  17511  1stckgenlem  17538  txbas  17552  txbasval  17591  tx1cn  17594  ptpjopn  17597  ptcnp  17607  txnlly  17622  txlm  17633  xkococn  17645  fgabs  17864  fmfnfmlem4  17942  flimcf  17967  hauspwpwf1  17972  fclsbas  18006  fclscf  18010  flimfnfcls  18013  ghmcnp  18097  tgpt0  18101  tsmsxp  18137  isxmet2d  18310  elmopn2  18428  mopni3  18477  blsscls2  18487  metequiv2  18493  metss2lem  18494  met2ndci  18505  metrest  18507  metcnp  18524  metcnp2  18525  metcnpi3  18529  txmetcnp  18530  isngp4  18611  nmolb2d  18705  xrge0tsms  18818  metdsre  18836  metnrmlem3  18844  addcnlem  18847  fsumcn  18853  elcncf2  18873  mulc1cncf  18888  cncfco  18890  cncfmet  18891  bndth  18936  evth  18937  copco  18996  pcopt2  19001  pcoass  19002  pcorevlem  19004  lmmcvg  19167  lmmbrf  19168  iscau4  19185  iscauf  19186  cmetcaulem  19194  iscmet3lem3  19196  iscmet3lem1  19197  causs  19204  equivcfil  19205  lmclim  19208  caubl  19213  caublcls  19214  bcth3  19237  ivthle  19306  ivthle2  19307  ovoliunlem1  19351  ovolicc2lem5  19370  volsuplem  19402  uniioombllem6  19433  dyaddisjlem  19440  dyadmax  19443  volcn  19451  mbfmulc2lem  19492  ismbf3d  19499  mbfsup  19509  mbfinf  19510  mbflim  19513  i1fmullem  19539  itg2seq  19587  itg2uba  19588  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  ditgsplitlem  19700  ellimc2  19717  ellimc3  19719  limcflf  19721  limcmpt  19723  limcco  19733  c1lip3  19836  lhop1lem  19850  dvfsumle  19858  dvfsumabs  19860  dvfsumrlim  19868  ftc1a  19874  ftc1lem6  19878  evlsval  19893  mdegmullem  19954  elply2  20068  plypf1  20084  aalioulem2  20203  aalioulem5  20206  aalioulem6  20207  aaliou  20208  ulmcaulem  20263  ulmcau  20264  ulmss  20266  ulmdvlem3  20271  mtest  20273  itgulm  20277  abelthlem8  20308  abelth  20310  tanord  20393  cxpcn3lem  20584  mcubic  20640  cubic2  20641  dvdsflsumcom  20926  fsumdvdsmul  20933  lgsdchrval  21084  2sqlem9  21110  rplogsumlem2  21132  rpvmasumlem  21134  dchrvmasumlem1  21142  vmalogdivsum2  21185  logsqvma  21189  selberg  21195  selberg4  21208  pntibndlem3  21239  pntlem3  21256  pntleml  21258  padicabv  21277  padicabvf  21278  padicabvcxp  21279  ostth3  21285  cusgrasize2inds  21439  grpolcan  21774  isgrp2d  21776  ghgrp  21909  nvmul0or  22086  sspival  22190  nmosetre  22218  blocnilem  22258  blocni  22259  h2hcau  22435  h2hlm  22436  shsel3  22770  chscllem2  23093  homulcl  23215  adjsym  23289  cnvadj  23348  hhcno  23360  hhcnf  23361  lnopl  23370  unoplin  23376  counop  23377  lnfnl  23387  hmoplin  23398  hmopm  23477  nmcexi  23482  lnconi  23489  riesz3i  23518  leopmuli  23589  leopmul  23590  hstle  23686  mdsl0  23766  mdslmd1lem2  23782  atcvatlem  23841  chirredi  23850  cdj1i  23889  isoun  24042  difioo  24098  gsumpropd2lem  24173  xrge0tsmsd  24176  pstmxmet  24245  dya2icoseg2  24581  ballotlemimin  24716  conpcon  24875  cvmliftmolem2  24922  cvmliftlem6  24930  cvmliftlem8  24932  cvmlift2lem10  24952  cvmlift2lem12  24954  relexpsucl  25085  relexpcnv  25086  relexpdm  25088  relexprn  25089  relexpadd  25091  relexpindlem  25092  rtrclreclem.trans  25099  rtrclreclem.min  25100  rtrclind  25102  dedekindle  25141  prodfn0  25175  prodfrec  25176  zprod  25216  fprodeq0  25252  fprodn0  25256  fprod2dlem  25257  dfon2lem6  25358  poseq  25467  nocvxminlem  25558  nofulllem4  25573  nofulllem5  25574  axpasch  25784  axcontlem7  25813  axcontlem10  25816  ifscgr  25882  brsegle  25946  itg2gt0cn  26159  bddiblnc  26174  ftc1cnnc  26178  comppfsc  26277  neibastop2lem  26279  cover2  26305  filbcmb  26332  fdc  26339  fdc1  26340  seqpo  26341  incsequz  26342  incsequz2  26343  metf1o  26351  lmclim2  26354  geomcau  26355  isbnd2  26382  bndss  26385  equivbnd  26389  ismtybndlem  26405  heibor1lem  26408  rrncmslem  26431  rrnequiv  26434  exidreslem  26442  ghomco  26448  isdrngo3  26465  rngoisocnv  26487  isidlc  26515  idlnegcl  26522  divrngidl  26528  intidl  26529  unichnidl  26531  keridl  26532  igenmin  26564  prnc  26567  ispridlc  26570  prter3  26621  lsmfgcl  27040  kercvrlsm  27049  frlmsslsp  27116  lindfmm  27165  islindf4  27176  hbt  27202  mamuass  27328  cntzsdrg  27378  climinf  27599  2spotdisj  28164  cotsqcscsq  28219  glbconxN  29860  atltcvr  29917  3dim1  29949  lvolnle3at  30064  linepsubN  30234  osumclN  30449  pexmidALTN  30460  lhpmatb  30513  cdlemg1idlemN  31054  dihlss  31733  dihglblem5aN  31775  dihatlat  31817
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