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

Theorem anassrs 648
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 605 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 432 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:  anass  649  mpanr1  683  pm2.61ddan  790  pm2.61dda  791  anass1rs  805  anabss5  812  anabss7  817  pm2.61da2ne  2767  2ralbida  2858  2rexbidva  2860  ralimdvva  2896  copsexg  4674  pofun  4755  imainss  5350  eqfnfv2  5897  fnex  6043  f1elima  6075  fliftfun  6104  isores2  6123  f1oiso  6141  ovmpt2dxf  6316  grpridd  6403  sorpssuni  6469  sorpssint  6470  tfindsg2  6572  oalim  7072  omlim  7073  oaass  7100  omlimcl  7117  omass  7119  oelim2  7134  oeoa  7136  oeoelem  7137  nnaass  7161  omabs  7186  eroveu  7295  sbthlem4  7524  fimaxg  7660  fisupg  7661  fofinf1o  7693  ordtypelem7  7839  hartogs  7859  card2on  7870  unwdomg  7900  wemapwe  8029  wemapweOLD  8030  dfac5  8399  cfsmolem  8540  isf32lem2  8624  ttukeylem6  8784  ondomon  8828  alephreg  8847  ltexprlem6  9311  recexsrlem  9371  dedekindle  9635  wloglei  9973  recextlem2  10068  fimaxre  10378  creur  10417  uzind3OLD  10838  uz11  10984  xrmaxeq  11252  xrmineq  11253  xaddf  11295  xaddass  11313  xleadd1a  11317  xlt2add  11324  xmullem  11328  xmulgt0  11347  xmulasslem3  11350  xlemul1a  11352  xadddilem  11358  fzrevral  11645  seqcaopr2  11943  expnlbnd2  12096  faclbnd4lem4  12173  shftlem  12659  01sqrex  12841  cau3lem  12944  limsupbnd2  13063  clim2  13084  clim2c  13085  clim0c  13087  rlimresb  13145  2clim  13152  climabs0  13165  climcn1  13171  climcn2  13172  o1rlimmul  13198  climsqz  13220  climsqz2  13221  rlimsqzlem  13228  lo1le  13231  climsup  13249  caucvgrlem2  13254  iseralt  13264  summolem2  13295  fsum2dlem  13339  cvgcmp  13381  cvgcmpce  13383  climfsum  13385  fsumiun  13386  geomulcvg  13438  mertenslem2  13447  mertens  13448  smu01lem  13783  gcdcllem1  13797  gcdmultiplez  13837  dvdssq  13846  coprmdvds2  13891  pclem  14007  pcge0  14030  pcgcd1  14045  prmpwdvds  14067  1arithlem4  14089  4sqlem18  14125  vdwlem10  14153  vdwlem11  14154  ramval  14171  ramub1lem2  14190  ramcl  14192  imasaddfnlem  14568  imasaddflem  14570  imasvscafn  14577  imasleval  14581  ismon2  14775  isepi2  14782  issubc3  14861  cofucl  14900  setcmon  15057  setcepi  15058  ipodrsfi  15435  ipodrsima  15437  isacs3lem  15438  grpidpropd  15549  mhmpropd  15572  mhmima  15593  gsumpropd2lem  15607  gsumccat  15621  grplcan  15692  mulgdirlem  15753  subgmulg  15797  issubg4  15802  subgint  15807  cycsubgcl  15809  ssnmz  15825  gastacl  15929  orbsta  15933  cntzsubg  15956  galactghm  16010  odmulg  16161  odbezout  16163  sylow3lem2  16231  lsmsubm  16256  efgsfo  16340  mulgmhm  16419  mulgghm  16420  gsumval3OLD  16486  gsumval3  16489  gsumcllem  16490  gsumcllemOLD  16491  gsumpt  16559  gsumptOLD  16560  gsum2d  16568  gsum2dOLD  16569  gsum2d2  16571  prdsgsum  16576  prdsgsumOLD  16577  subgdmdprd  16636  dprd2d2  16648  ablfac1eu  16679  srglmhm  16739  srgrmhm  16740  rngpropd  16782  rnglghm  16799  dvdsrpropd  16894  abvpropd  17033  islmodd  17060  lmodprop2d  17113  lsssubg  17144  lsspropd  17204  islmhm2  17225  lmhmima  17234  lsmelval2  17272  lidlsubg  17403  assapropd  17504  asclpropd  17522  psrass1lem  17553  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  mplind  17691  evlslem2  17704  evlsval  17712  coe1tmmul2  17837  phlpropd  18193  frlmsslsp  18332  frlmsslspOLD  18333  lindfmm  18365  islindf4  18376  mamuass  18415  mavmulass  18471  mdetuni0  18543  mdetmul  18545  neips  18833  neindisj  18837  ordtrest2lem  18923  lmbrf  18980  lmss  19018  isreg2  19097  lmmo  19100  hauscmplem  19125  bwth  19129  2ndcomap  19178  1stcelcls  19181  restlly  19203  islly2  19204  cldllycmp  19215  1stckgenlem  19242  txbas  19256  txbasval  19295  tx1cn  19298  ptpjopn  19301  ptcnp  19311  txnlly  19326  txlm  19337  xkococn  19349  fgabs  19568  fmfnfmlem4  19646  flimcf  19671  hauspwpwf1  19676  fclsbas  19710  fclscf  19714  flimfnfcls  19717  ghmcnp  19801  tgpt0  19805  tsmsxp  19845  isxmet2d  20018  elmopn2  20136  mopni3  20185  blsscls2  20195  metequiv2  20201  metss2lem  20202  met2ndci  20213  metrest  20215  metcnp  20232  metcnp2  20233  metcnpi3  20237  txmetcnp  20238  isngp4  20319  nmolb2d  20413  xrge0tsms  20527  metdsre  20545  metnrmlem3  20553  addcnlem  20556  fsumcn  20562  elcncf2  20582  mulc1cncf  20597  cncfco  20599  cncfmet  20600  bndth  20646  evth  20647  copco  20706  pcopt2  20711  pcoass  20712  pcorevlem  20714  lmmcvg  20888  lmmbrf  20889  iscau4  20906  iscauf  20907  cmetcaulem  20915  iscmet3lem3  20917  iscmet3lem1  20918  causs  20925  equivcfil  20926  lmclim  20929  caubl  20934  caublcls  20935  bcth3  20958  ivthle  21056  ivthle2  21057  ovoliunlem1  21101  ovolicc2lem5  21120  volsuplem  21152  uniioombllem6  21184  dyaddisjlem  21191  dyadmax  21194  volcn  21202  mbfmulc2lem  21241  ismbf3d  21248  mbfsup  21258  mbfinf  21259  mbflim  21262  i1fmullem  21288  itg2seq  21336  itg2uba  21337  itg2splitlem  21342  itg2split  21343  itg2monolem1  21344  ditgsplitlem  21451  ellimc2  21468  ellimc3  21470  limcflf  21472  limcmpt  21474  limcco  21484  c1lip3  21587  lhop1lem  21601  dvfsumle  21609  dvfsumabs  21611  dvfsumrlim  21619  ftc1a  21625  ftc1lem6  21629  mdegmullem  21665  elply2  21780  plypf1  21796  aalioulem2  21915  aalioulem5  21918  aalioulem6  21919  aaliou  21920  ulmcaulem  21975  ulmcau  21976  ulmss  21978  ulmdvlem3  21983  mtest  21985  itgulm  21989  abelthlem8  22020  abelth  22022  tanord  22110  cxpcn3lem  22301  mcubic  22358  cubic2  22359  dvdsflsumcom  22644  fsumdvdsmul  22651  lgsdchrval  22802  2sqlem9  22828  rplogsumlem2  22850  rpvmasumlem  22852  dchrvmasumlem1  22860  vmalogdivsum2  22903  logsqvma  22907  selberg  22913  selberg4  22926  pntibndlem3  22957  pntlem3  22974  pntleml  22976  padicabv  22995  padicabvf  22996  padicabvcxp  22997  ostth3  23003  axpasch  23322  axcontlem7  23351  axcontlem10  23354  cusgrasize2inds  23520  grpolcan  23855  isgrp2d  23857  ghgrp  23990  nvmul0or  24167  sspival  24271  nmosetre  24299  blocnilem  24339  blocni  24340  h2hcau  24516  h2hlm  24517  shsel3  24853  chscllem2  25176  homulcl  25298  adjsym  25372  cnvadj  25431  hhcno  25443  hhcnf  25444  lnopl  25453  unoplin  25459  counop  25460  lnfnl  25470  hmoplin  25481  hmopm  25560  nmcexi  25565  lnconi  25572  riesz3i  25601  leopmuli  25672  leopmul  25673  hstle  25769  mdsl0  25849  mdslmd1lem2  25865  atcvatlem  25924  chirredi  25933  cdj1i  25972  isoun  26131  difioo  26206  xrge0tsmsd  26387  pstmxmet  26458  ordtrest2NEWlem  26486  dya2icoseg2  26827  eulerpartlemgc  26879  eulerpartlemgvv  26893  eulerpartlemgh  26895  eulerpartlemgs2  26897  ballotlemimin  27022  signstfvneq0  27107  conpcon  27258  cvmliftmolem2  27305  cvmliftlem6  27313  cvmliftlem8  27315  cvmlift2lem10  27335  cvmlift2lem12  27337  relexpsucl  27468  relexpcnv  27469  relexpdm  27471  relexprn  27472  relexpadd  27474  relexpindlem  27475  rtrclreclem.trans  27482  rtrclreclem.min  27483  rtrclind  27485  prodfn0  27543  prodfrec  27544  zprod  27584  fprodeq0  27620  fprodn0  27624  fprod2dlem  27625  dfon2lem6  27735  poseq  27848  nocvxminlem  27965  nofulllem4  27980  nofulllem5  27981  ifscgr  28209  brsegle  28273  finixpnum  28552  fin2solem  28553  fin2so  28554  heicant  28564  itg2gt0cn  28585  bddiblnc  28600  ftc1cnnc  28604  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anc  28613  comppfsc  28717  neibastop2lem  28719  cover2  28745  filbcmb  28772  fdc  28779  fdc1  28780  seqpo  28781  incsequz  28782  incsequz2  28783  metf1o  28789  lmclim2  28792  geomcau  28793  isbnd2  28820  bndss  28823  equivbnd  28827  ismtybndlem  28843  heibor1lem  28846  rrncmslem  28869  rrnequiv  28872  exidreslem  28880  ghomco  28886  isdrngo3  28903  rngoisocnv  28925  isidlc  28953  idlnegcl  28960  divrngidl  28966  intidl  28967  unichnidl  28969  keridl  28970  igenmin  29002  prnc  29005  ispridlc  29008  prter3  29165  lsmfgcl  29565  kercvrlsm  29574  unxpwdom3  29586  hbt  29624  cntzsdrg  29697  climinf  29917  2spotdisj  30792  ovmpt2rdxf  30867  scmatscmid  31011  cpmatacl  31179  cpmadugsumfi  31331  cpmadugsum  31332  cpmadumatpolylem1  31335  cpmadumatpolylem3  31337  cpmadumatpoly  31338  cayhamlem4  31343  cotsqcscsq  31393  glbconxN  33328  atltcvr  33385  3dim1  33417  lvolnle3at  33532  linepsubN  33702  osumclN  33917  pexmidALTN  33928  lhpmatb  33981  cdlemg1idlemN  34522  dihlss  35201  dihglblem5aN  35243  dihatlat  35285
  Copyright terms: Public domain W3C validator