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  2677  2ralbida  2736  2rexbidva  2738  pofun  4511  tfindsg2  4832  imainss  5278  eqfnfv2  5819  fnex  5952  f1elima  6000  fliftfun  6025  isores2  6044  f1oiso  6062  ovmpt2dxf  6190  grpridd  6278  sorpssuni  6522  sorpssint  6523  oalim  6767  omlim  6768  oaass  6795  omlimcl  6812  omass  6814  oelim2  6829  oeoa  6831  oeoelem  6832  nnaass  6856  omabs  6881  eroveu  6990  sbthlem4  7211  fimaxg  7345  fisupg  7346  fofinf1o  7378  ordtypelem7  7482  hartogs  7502  card2on  7511  unwdomg  7541  wemapwe  7643  dfac5  7998  cfsmolem  8139  isf32lem2  8223  ttukeylem6  8383  ondomon  8427  alephreg  8446  ltexprlem6  8907  recexsrlem  8967  wloglei  9548  recextlem2  9642  fimaxre  9944  creur  9983  uzind3OLD  10354  uz11  10497  xrmaxeq  10756  xrmineq  10757  xaddf  10799  xaddass  10817  xleadd1a  10821  xlt2add  10828  xmullem  10832  xmulgt0  10851  xmulasslem3  10854  xlemul1a  10856  xadddilem  10862  fzrevral  11119  seqcaopr2  11347  expnlbnd2  11498  faclbnd4lem4  11575  shftlem  11871  01sqrex  12043  cau3lem  12146  limsupbnd2  12265  clim2  12286  clim2c  12287  clim0c  12289  rlimresb  12347  2clim  12354  climabs0  12367  climcn1  12373  climcn2  12374  o1rlimmul  12400  climsqz  12422  climsqz2  12423  rlimsqzlem  12430  lo1le  12433  climsup  12451  caucvgrlem2  12456  iseralt  12466  summolem2  12498  fsum2dlem  12542  cvgcmp  12583  cvgcmpce  12585  climfsum  12587  fsumiun  12588  geomulcvg  12641  mertenslem2  12650  mertens  12651  smu01lem  12985  gcdcllem1  12999  gcdmultiplez  13039  dvdssq  13048  coprmdvds2  13091  pclem  13200  pcge0  13223  pcgcd1  13238  prmpwdvds  13260  1arithlem4  13282  4sqlem18  13318  vdwlem10  13346  vdwlem11  13347  ramval  13364  ramub1lem2  13383  ramcl  13385  imasaddfnlem  13741  imasaddflem  13743  imasvscafn  13750  imasleval  13754  ismon2  13948  isepi2  13955  issubc3  14034  cofucl  14073  setcmon  14230  setcepi  14231  ipodrsfi  14577  ipodrsima  14579  isacs3lem  14580  grpidpropd  14710  mhmpropd  14732  mhmima  14751  gsumccat  14775  grplcan  14845  mulgdirlem  14902  subgmulg  14946  issubg4  14949  subgint  14952  cycsubgcl  14954  ssnmz  14970  gastacl  15074  orbsta  15078  galactghm  15094  cntzsubg  15123  odmulg  15180  odbezout  15182  sylow3lem2  15250  lsmsubm  15275  efgsfo  15359  mulgmhm  15438  mulgghm  15439  gsumval3  15502  gsumcllem  15504  gsumpt  15533  gsum2d  15534  gsum2d2  15536  prdsgsum  15540  subgdmdprd  15580  dprd2d2  15590  ablfac1eu  15619  rngpropd  15683  rnglghm  15699  dvdsrpropd  15789  abvpropd  15918  islmodd  15944  lmodprop2d  15994  lsssubg  16021  lsspropd  16081  islmhm2  16102  lmhmima  16111  lsmelval2  16145  lidlsubg  16274  assapropd  16374  asclpropd  16392  psrass1lem  16430  mplcoe1  16516  mplcoe2  16518  mplind  16550  evlslem2  16556  coe1tmmul2  16656  phlpropd  16874  neips  17165  neindisj  17169  ordtrest2lem  17255  lmbrf  17312  lmss  17350  isreg2  17429  lmmo  17432  hauscmplem  17457  2ndcomap  17509  1stcelcls  17512  restlly  17534  islly2  17535  cldllycmp  17546  1stckgenlem  17573  txbas  17587  txbasval  17626  tx1cn  17629  ptpjopn  17632  ptcnp  17642  txnlly  17657  txlm  17668  xkococn  17680  fgabs  17899  fmfnfmlem4  17977  flimcf  18002  hauspwpwf1  18007  fclsbas  18041  fclscf  18045  flimfnfcls  18048  ghmcnp  18132  tgpt0  18136  tsmsxp  18172  isxmet2d  18345  elmopn2  18463  mopni3  18512  blsscls2  18522  metequiv2  18528  metss2lem  18529  met2ndci  18540  metrest  18542  metcnp  18559  metcnp2  18560  metcnpi3  18564  txmetcnp  18565  isngp4  18646  nmolb2d  18740  xrge0tsms  18853  metdsre  18871  metnrmlem3  18879  addcnlem  18882  fsumcn  18888  elcncf2  18908  mulc1cncf  18923  cncfco  18925  cncfmet  18926  bndth  18971  evth  18972  copco  19031  pcopt2  19036  pcoass  19037  pcorevlem  19039  lmmcvg  19202  lmmbrf  19203  iscau4  19220  iscauf  19221  cmetcaulem  19229  iscmet3lem3  19231  iscmet3lem1  19232  causs  19239  equivcfil  19240  lmclim  19243  caubl  19248  caublcls  19249  bcth3  19272  ivthle  19341  ivthle2  19342  ovoliunlem1  19386  ovolicc2lem5  19405  volsuplem  19437  uniioombllem6  19468  dyaddisjlem  19475  dyadmax  19478  volcn  19486  mbfmulc2lem  19527  ismbf3d  19534  mbfsup  19544  mbfinf  19545  mbflim  19548  i1fmullem  19574  itg2seq  19622  itg2uba  19623  itg2splitlem  19628  itg2split  19629  itg2monolem1  19630  ditgsplitlem  19735  ellimc2  19752  ellimc3  19754  limcflf  19756  limcmpt  19758  limcco  19768  c1lip3  19871  lhop1lem  19885  dvfsumle  19893  dvfsumabs  19895  dvfsumrlim  19903  ftc1a  19909  ftc1lem6  19913  evlsval  19928  mdegmullem  19989  elply2  20103  plypf1  20119  aalioulem2  20238  aalioulem5  20241  aalioulem6  20242  aaliou  20243  ulmcaulem  20298  ulmcau  20299  ulmss  20301  ulmdvlem3  20306  mtest  20308  itgulm  20312  abelthlem8  20343  abelth  20345  tanord  20428  cxpcn3lem  20619  mcubic  20675  cubic2  20676  dvdsflsumcom  20961  fsumdvdsmul  20968  lgsdchrval  21119  2sqlem9  21145  rplogsumlem2  21167  rpvmasumlem  21169  dchrvmasumlem1  21177  vmalogdivsum2  21220  logsqvma  21224  selberg  21230  selberg4  21243  pntibndlem3  21274  pntlem3  21291  pntleml  21293  padicabv  21312  padicabvf  21313  padicabvcxp  21314  ostth3  21320  cusgrasize2inds  21474  grpolcan  21809  isgrp2d  21811  ghgrp  21944  nvmul0or  22121  sspival  22225  nmosetre  22253  blocnilem  22293  blocni  22294  h2hcau  22470  h2hlm  22471  shsel3  22805  chscllem2  23128  homulcl  23250  adjsym  23324  cnvadj  23383  hhcno  23395  hhcnf  23396  lnopl  23405  unoplin  23411  counop  23412  lnfnl  23422  hmoplin  23433  hmopm  23512  nmcexi  23517  lnconi  23524  riesz3i  23553  leopmuli  23624  leopmul  23625  hstle  23721  mdsl0  23801  mdslmd1lem2  23817  atcvatlem  23876  chirredi  23885  cdj1i  23924  isoun  24077  difioo  24133  gsumpropd2lem  24208  xrge0tsmsd  24211  pstmxmet  24280  dya2icoseg2  24616  ballotlemimin  24751  conpcon  24910  cvmliftmolem2  24957  cvmliftlem6  24965  cvmliftlem8  24967  cvmlift2lem10  24987  cvmlift2lem12  24989  relexpsucl  25120  relexpcnv  25121  relexpdm  25123  relexprn  25124  relexpadd  25126  relexpindlem  25127  rtrclreclem.trans  25134  rtrclreclem.min  25135  rtrclind  25137  dedekindle  25176  prodfn0  25211  prodfrec  25212  zprod  25252  fprodeq0  25288  fprodn0  25292  fprod2dlem  25293  dfon2lem6  25399  poseq  25508  nocvxminlem  25599  nofulllem4  25614  nofulllem5  25615  axpasch  25828  axcontlem7  25857  axcontlem10  25860  ifscgr  25926  brsegle  25990  itg2gt0cn  26206  bddiblnc  26221  ftc1cnnc  26225  comppfsc  26324  neibastop2lem  26326  cover2  26352  filbcmb  26379  fdc  26386  fdc1  26387  seqpo  26388  incsequz  26389  incsequz2  26390  metf1o  26398  lmclim2  26401  geomcau  26402  isbnd2  26429  bndss  26432  equivbnd  26436  ismtybndlem  26452  heibor1lem  26455  rrncmslem  26478  rrnequiv  26481  exidreslem  26489  ghomco  26495  isdrngo3  26512  rngoisocnv  26534  isidlc  26562  idlnegcl  26569  divrngidl  26575  intidl  26576  unichnidl  26578  keridl  26579  igenmin  26611  prnc  26614  ispridlc  26617  prter3  26668  lsmfgcl  27087  kercvrlsm  27096  frlmsslsp  27163  lindfmm  27212  islindf4  27223  hbt  27249  mamuass  27375  cntzsdrg  27425  climinf  27646  2spotdisj  28308  cotsqcscsq  28363  glbconxN  30014  atltcvr  30071  3dim1  30103  lvolnle3at  30218  linepsubN  30388  osumclN  30603  pexmidALTN  30614  lhpmatb  30667  cdlemg1idlemN  31208  dihlss  31887  dihglblem5aN  31929  dihatlat  31971
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