MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anassrs Structured version   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  4833  imainss  5279  eqfnfv2  5820  fnex  5953  f1elima  6001  fliftfun  6026  isores2  6045  f1oiso  6063  ovmpt2dxf  6191  grpridd  6279  sorpssuni  6523  sorpssint  6524  oalim  6768  omlim  6769  oaass  6796  omlimcl  6813  omass  6815  oelim2  6830  oeoa  6832  oeoelem  6833  nnaass  6857  omabs  6882  eroveu  6991  sbthlem4  7212  fimaxg  7346  fisupg  7347  fofinf1o  7379  ordtypelem7  7483  hartogs  7503  card2on  7512  unwdomg  7542  wemapwe  7644  dfac5  7999  cfsmolem  8140  isf32lem2  8224  ttukeylem6  8384  ondomon  8428  alephreg  8447  ltexprlem6  8908  recexsrlem  8968  wloglei  9549  recextlem2  9643  fimaxre  9945  creur  9984  uzind3OLD  10355  uz11  10498  xrmaxeq  10757  xrmineq  10758  xaddf  10800  xaddass  10818  xleadd1a  10822  xlt2add  10829  xmullem  10833  xmulgt0  10852  xmulasslem3  10855  xlemul1a  10857  xadddilem  10863  fzrevral  11121  seqcaopr2  11349  expnlbnd2  11500  faclbnd4lem4  11577  shftlem  11873  01sqrex  12045  cau3lem  12148  limsupbnd2  12267  clim2  12288  clim2c  12289  clim0c  12291  rlimresb  12349  2clim  12356  climabs0  12369  climcn1  12375  climcn2  12376  o1rlimmul  12402  climsqz  12424  climsqz2  12425  rlimsqzlem  12432  lo1le  12435  climsup  12453  caucvgrlem2  12458  iseralt  12468  summolem2  12500  fsum2dlem  12544  cvgcmp  12585  cvgcmpce  12587  climfsum  12589  fsumiun  12590  geomulcvg  12643  mertenslem2  12652  mertens  12653  smu01lem  12987  gcdcllem1  13001  gcdmultiplez  13041  dvdssq  13050  coprmdvds2  13093  pclem  13202  pcge0  13225  pcgcd1  13240  prmpwdvds  13262  1arithlem4  13284  4sqlem18  13320  vdwlem10  13348  vdwlem11  13349  ramval  13366  ramub1lem2  13385  ramcl  13387  imasaddfnlem  13743  imasaddflem  13745  imasvscafn  13752  imasleval  13756  ismon2  13950  isepi2  13957  issubc3  14036  cofucl  14075  setcmon  14232  setcepi  14233  ipodrsfi  14579  ipodrsima  14581  isacs3lem  14582  grpidpropd  14712  mhmpropd  14734  mhmima  14753  gsumccat  14777  grplcan  14847  mulgdirlem  14904  subgmulg  14948  issubg4  14951  subgint  14954  cycsubgcl  14956  ssnmz  14972  gastacl  15076  orbsta  15080  galactghm  15096  cntzsubg  15125  odmulg  15182  odbezout  15184  sylow3lem2  15252  lsmsubm  15277  efgsfo  15361  mulgmhm  15440  mulgghm  15441  gsumval3  15504  gsumcllem  15506  gsumpt  15535  gsum2d  15536  gsum2d2  15538  prdsgsum  15542  subgdmdprd  15582  dprd2d2  15592  ablfac1eu  15621  rngpropd  15685  rnglghm  15701  dvdsrpropd  15791  abvpropd  15920  islmodd  15946  lmodprop2d  15996  lsssubg  16023  lsspropd  16083  islmhm2  16104  lmhmima  16113  lsmelval2  16147  lidlsubg  16276  assapropd  16376  asclpropd  16394  psrass1lem  16432  mplcoe1  16518  mplcoe2  16520  mplind  16552  evlslem2  16558  coe1tmmul2  16658  phlpropd  16876  neips  17167  neindisj  17171  ordtrest2lem  17257  lmbrf  17314  lmss  17352  isreg2  17431  lmmo  17434  hauscmplem  17459  2ndcomap  17511  1stcelcls  17514  restlly  17536  islly2  17537  cldllycmp  17548  1stckgenlem  17575  txbas  17589  txbasval  17628  tx1cn  17631  ptpjopn  17634  ptcnp  17644  txnlly  17659  txlm  17670  xkococn  17682  fgabs  17901  fmfnfmlem4  17979  flimcf  18004  hauspwpwf1  18009  fclsbas  18043  fclscf  18047  flimfnfcls  18050  ghmcnp  18134  tgpt0  18138  tsmsxp  18174  isxmet2d  18347  elmopn2  18465  mopni3  18514  blsscls2  18524  metequiv2  18530  metss2lem  18531  met2ndci  18542  metrest  18544  metcnp  18561  metcnp2  18562  metcnpi3  18566  txmetcnp  18567  isngp4  18648  nmolb2d  18742  xrge0tsms  18855  metdsre  18873  metnrmlem3  18881  addcnlem  18884  fsumcn  18890  elcncf2  18910  mulc1cncf  18925  cncfco  18927  cncfmet  18928  bndth  18973  evth  18974  copco  19033  pcopt2  19038  pcoass  19039  pcorevlem  19041  lmmcvg  19204  lmmbrf  19205  iscau4  19222  iscauf  19223  cmetcaulem  19231  iscmet3lem3  19233  iscmet3lem1  19234  causs  19241  equivcfil  19242  lmclim  19245  caubl  19250  caublcls  19251  bcth3  19274  ivthle  19343  ivthle2  19344  ovoliunlem1  19388  ovolicc2lem5  19407  volsuplem  19439  uniioombllem6  19470  dyaddisjlem  19477  dyadmax  19480  volcn  19488  mbfmulc2lem  19529  ismbf3d  19536  mbfsup  19546  mbfinf  19547  mbflim  19550  i1fmullem  19576  itg2seq  19624  itg2uba  19625  itg2splitlem  19630  itg2split  19631  itg2monolem1  19632  ditgsplitlem  19737  ellimc2  19754  ellimc3  19756  limcflf  19758  limcmpt  19760  limcco  19770  c1lip3  19873  lhop1lem  19887  dvfsumle  19895  dvfsumabs  19897  dvfsumrlim  19905  ftc1a  19911  ftc1lem6  19915  evlsval  19930  mdegmullem  19991  elply2  20105  plypf1  20121  aalioulem2  20240  aalioulem5  20243  aalioulem6  20244  aaliou  20245  ulmcaulem  20300  ulmcau  20301  ulmss  20303  ulmdvlem3  20308  mtest  20310  itgulm  20314  abelthlem8  20345  abelth  20347  tanord  20430  cxpcn3lem  20621  mcubic  20677  cubic2  20678  dvdsflsumcom  20963  fsumdvdsmul  20970  lgsdchrval  21121  2sqlem9  21147  rplogsumlem2  21169  rpvmasumlem  21171  dchrvmasumlem1  21179  vmalogdivsum2  21222  logsqvma  21226  selberg  21232  selberg4  21245  pntibndlem3  21276  pntlem3  21293  pntleml  21295  padicabv  21314  padicabvf  21315  padicabvcxp  21316  ostth3  21322  cusgrasize2inds  21476  grpolcan  21811  isgrp2d  21813  ghgrp  21946  nvmul0or  22123  sspival  22227  nmosetre  22255  blocnilem  22295  blocni  22296  h2hcau  22472  h2hlm  22473  shsel3  22807  chscllem2  23130  homulcl  23252  adjsym  23326  cnvadj  23385  hhcno  23397  hhcnf  23398  lnopl  23407  unoplin  23413  counop  23414  lnfnl  23424  hmoplin  23435  hmopm  23514  nmcexi  23519  lnconi  23526  riesz3i  23555  leopmuli  23626  leopmul  23627  hstle  23723  mdsl0  23803  mdslmd1lem2  23819  atcvatlem  23878  chirredi  23887  cdj1i  23926  isoun  24079  difioo  24135  gsumpropd2lem  24210  xrge0tsmsd  24213  pstmxmet  24282  dya2icoseg2  24618  ballotlemimin  24753  conpcon  24912  cvmliftmolem2  24959  cvmliftlem6  24967  cvmliftlem8  24969  cvmlift2lem10  24989  cvmlift2lem12  24991  relexpsucl  25122  relexpcnv  25123  relexpdm  25125  relexprn  25126  relexpadd  25128  relexpindlem  25129  rtrclreclem.trans  25136  rtrclreclem.min  25137  rtrclind  25139  dedekindle  25178  prodfn0  25212  prodfrec  25213  zprod  25253  fprodeq0  25289  fprodn0  25293  fprod2dlem  25294  dfon2lem6  25403  poseq  25513  nocvxminlem  25610  nofulllem4  25625  nofulllem5  25626  axpasch  25845  axcontlem7  25874  axcontlem10  25877  ifscgr  25943  brsegle  26007  itg2gt0cn  26223  bddiblnc  26238  ftc1cnnc  26242  comppfsc  26341  neibastop2lem  26343  cover2  26369  filbcmb  26396  fdc  26403  fdc1  26404  seqpo  26405  incsequz  26406  incsequz2  26407  metf1o  26415  lmclim2  26418  geomcau  26419  isbnd2  26446  bndss  26449  equivbnd  26453  ismtybndlem  26469  heibor1lem  26472  rrncmslem  26495  rrnequiv  26498  exidreslem  26506  ghomco  26512  isdrngo3  26529  rngoisocnv  26551  isidlc  26579  idlnegcl  26586  divrngidl  26592  intidl  26593  unichnidl  26595  keridl  26596  igenmin  26628  prnc  26631  ispridlc  26634  prter3  26685  lsmfgcl  27104  kercvrlsm  27113  frlmsslsp  27180  lindfmm  27229  islindf4  27240  hbt  27266  mamuass  27392  cntzsdrg  27442  climinf  27663  2spotdisj  28351  cotsqcscsq  28406  glbconxN  30076  atltcvr  30133  3dim1  30165  lvolnle3at  30280  linepsubN  30450  osumclN  30665  pexmidALTN  30676  lhpmatb  30729  cdlemg1idlemN  31270  dihlss  31949  dihglblem5aN  31991  dihatlat  32033
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