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

Theorem anassrs 678
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anassrs.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
anassrs (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem anassrs
StepHypRef Expression
1 anassrs.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21exp32 629 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 447 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  anass  679  mpanr1  715  pm2.61ddan  829  pm2.61dda  830  anass1rs  845  anabss5  853  anabss7  858  pm2.61da2ne  2870  ralimdvva  2947  2ralbida  2970  2ralbidva  2971  2rexbidva  3038  copsexg  4882  pofun  4975  imainss  5467  eqfnfv2  6220  fnex  6386  f1elima  6421  fliftfun  6462  isores2  6483  f1oiso  6501  ovmpt2dxf  6684  grpridd  6772  sorpssuni  6844  sorpssint  6845  tfindsg2  6953  oalim  7499  omlim  7500  oaass  7528  omlimcl  7545  omass  7547  oelim2  7562  oeoa  7564  oeoelem  7565  nnaass  7589  omabs  7614  eroveu  7729  sbthlem4  7958  fimaxg  8092  fisupg  8093  fofinf1o  8126  fiming  8287  fiinfg  8288  ordtypelem7  8312  hartogs  8332  card2on  8342  unwdomg  8372  wemapwe  8477  dfac5  8834  cfsmolem  8975  isf32lem2  9059  ttukeylem6  9219  ondomon  9264  alephreg  9283  ltexprlem6  9742  recexsrlem  9803  wloglei  10439  recextlem2  10537  fimaxre  10847  creur  10891  uz11  11586  xrmaxeq  11884  xrmineq  11885  xaddf  11929  xaddass  11951  xleadd1a  11955  xlt2add  11962  xmullem  11966  xmulgt0  11985  xmulasslem3  11988  xlemul1a  11990  xadddilem  11996  fzrevral  12294  seqcaopr2  12699  expnlbnd2  12857  faclbnd4lem4  12945  rtrclreclem3  13648  rtrclreclem4  13649  relexpindlem  13651  rtrclind  13653  shftlem  13656  01sqrex  13838  cau3lem  13942  limsupbnd2  14062  clim2  14083  clim2c  14084  clim0c  14086  rlimresb  14144  2clim  14151  climabs0  14164  climcn1  14170  climcn2  14171  o1rlimmul  14197  climsqz  14219  climsqz2  14220  rlimsqzlem  14227  lo1le  14230  climsup  14248  caucvgrlem2  14253  iseralt  14263  summolem2  14294  fsum2dlem  14343  cvgcmp  14389  cvgcmpce  14391  climfsum  14393  fsumiun  14394  geomulcvg  14446  mertenslem2  14456  mertens  14457  prodfn0  14465  prodfrec  14466  zprod  14506  fprodeq0  14544  fprodn0  14548  fprod2dlem  14549  smu01lem  15045  gcdcllem1  15059  gcdmultiplez  15108  dvdssq  15118  lcmgcdlem  15157  lcmdvds  15159  coprmdvds2  15206  pclem  15381  pcge0  15404  pcgcd1  15419  prmpwdvds  15446  1arithlem4  15468  4sqlem18  15504  vdwlem10  15532  vdwlem11  15533  ramval  15550  ramub1lem2  15569  ramcl  15571  imasaddfnlem  16011  imasaddflem  16013  imasvscafn  16020  imasleval  16024  ismon2  16217  isepi2  16224  issubc3  16332  cofucl  16371  setcmon  16560  setcepi  16561  ipodrsfi  16986  ipodrsima  16988  isacs3lem  16989  grpidpropd  17084  gsumpropd2lem  17096  mhmpropd  17164  mhmima  17186  gsumccat  17201  grplcan  17300  dfgrp3lem  17336  mulgdirlem  17395  subgmulg  17431  issubg4  17436  subgint  17441  cycsubgcl  17443  ssnmz  17459  gastacl  17565  orbsta  17569  cntzsubg  17592  galactghm  17646  odmulg  17796  odbezout  17798  sylow3lem2  17866  lsmsubm  17891  efgsfo  17975  mulgmhm  18056  mulgghm  18057  gsumval3  18131  gsumcllem  18132  gsumpt  18184  gsum2d  18194  gsum2d2  18196  prdsgsum  18200  subgdmdprd  18256  dprd2d2  18266  ablfac1eu  18295  srglmhm  18358  srgrmhm  18359  ringpropd  18405  ringlghm  18427  dvdsrpropd  18519  abvpropd  18665  islmodd  18692  lmodprop2d  18748  lsssubg  18778  lsspropd  18838  lmhmima  18868  lsmelval2  18906  lidlsubg  19036  assapropd  19148  asclpropd  19167  psrass1lem  19198  mplcoe1  19286  mplcoe5  19289  mplind  19323  evlslem2  19333  evlsval  19340  coe1tmmul2  19467  phlpropd  19819  frlmsslsp  19954  lindfmm  19985  islindf4  19996  mamuass  20027  mavmulass  20174  mdetuni0  20246  mdetmul  20248  cpmatacl  20340  cpmadugsumfi  20501  cpmadugsum  20502  cpmadumatpolylem1  20505  cpmadumatpolylem2  20506  cpmadumatpoly  20507  cayhamlem4  20512  neips  20727  neindisj  20731  ordtrest2lem  20817  lmbrf  20874  lmss  20912  isreg2  20991  lmmo  20994  hauscmplem  21019  bwth  21023  2ndcomap  21071  1stcelcls  21074  restlly  21096  islly2  21097  cldllycmp  21108  comppfsc  21145  1stckgenlem  21166  txbas  21180  txbasval  21219  tx1cn  21222  ptpjopn  21225  ptcnp  21235  txnlly  21250  txlm  21261  xkococn  21273  fgabs  21493  fmfnfmlem4  21571  flimcf  21596  hauspwpwf1  21601  fclsbas  21635  fclscf  21639  flimfnfcls  21642  ghmcnp  21728  tsmsxp  21768  isxmet2d  21942  elmopn2  22060  mopni3  22109  blsscls2  22119  metequiv2  22125  metss2lem  22126  met2ndci  22137  metrest  22139  metcnp  22156  metcnp2  22157  metcnpi3  22161  txmetcnp  22162  nmolb2d  22332  xrge0tsms  22445  metdsre  22464  metnrmlem3  22472  fsumcn  22481  elcncf2  22501  mulc1cncf  22516  cncfco  22518  cncfmet  22519  bndth  22565  evth  22566  copco  22626  pcopt2  22631  pcoass  22632  pcorevlem  22634  lmmcvg  22867  lmmbrf  22868  iscau4  22885  iscauf  22886  cmetcaulem  22894  iscmet3lem3  22896  iscmet3lem1  22897  causs  22904  equivcfil  22905  lmclim  22909  caubl  22914  caublcls  22915  bcth3  22936  ivthle  23032  ivthle2  23033  ovoliunlem1  23077  ovolicc2lem5  23096  volsuplem  23130  uniioombllem6  23162  dyaddisjlem  23169  dyadmax  23172  volcn  23180  mbfmulc2lem  23220  ismbf3d  23227  mbfsup  23237  mbfinf  23238  mbflim  23241  i1fmullem  23267  itg2seq  23315  itg2uba  23316  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  ditgsplitlem  23430  ellimc2  23447  ellimc3  23449  limcflf  23451  limcmpt  23453  limcco  23463  lhop1lem  23580  dvfsumle  23588  dvfsumabs  23590  dvfsumrlim  23598  ftc1a  23604  ftc1lem6  23608  mdegmullem  23642  elply2  23756  plypf1  23772  ulmcaulem  23952  ulmcau  23953  ulmss  23955  ulmdvlem3  23960  mtest  23962  itgulm  23966  abelthlem8  23997  abelth  23999  tanord  24088  cxpcn3lem  24288  mcubic  24374  cubic2  24375  dvdsflsumcom  24714  fsumdvdsmul  24721  lgsdchrval  24879  2sqlem9  24952  rplogsumlem2  24974  rpvmasumlem  24976  dchrvmasumlem1  24984  vmalogdivsum2  25027  logsqvma  25031  selberg  25037  selberg4  25050  pntibndlem3  25081  pntlem3  25098  pntleml  25100  padicabv  25119  padicabvf  25120  padicabvcxp  25121  ostth3  25127  axpasch  25621  axcontlem7  25650  axcontlem10  25653  cusgrasize2inds  26005  2spotdisj  26588  grpolcan  26768  nvmul0or  26889  nmosetre  27003  blocnilem  27043  blocni  27044  h2hcau  27220  h2hlm  27221  shsel3  27558  chscllem2  27881  homulcl  28002  adjsym  28076  cnvadj  28135  hhcno  28147  hhcnf  28148  lnopl  28157  unoplin  28163  counop  28164  lnfnl  28174  hmoplin  28185  hmopm  28264  nmcexi  28269  lnconi  28276  riesz3i  28305  leopmuli  28376  leopmul  28377  hstle  28473  mdsl0  28553  mdslmd1lem2  28569  atcvatlem  28628  chirredi  28637  cdj1i  28676  foresf1o  28727  isoun  28862  difioo  28934  xrge0tsmsd  29116  pstmxmet  29268  ordtrest2NEWlem  29296  esum2dlem  29481  esum2d  29482  dya2icoseg2  29667  eulerpartlemgc  29751  eulerpartlemgvv  29765  eulerpartlemgh  29767  eulerpartlemgs2  29769  ballotlemimin  29894  signstfvneq0  29975  conpcon  30471  cvmliftmolem2  30518  cvmliftlem6  30526  cvmliftlem8  30528  cvmlift2lem10  30548  cvmlift2lem12  30550  elmrsubrn  30671  dfon2lem6  30937  poseq  30994  nocvxminlem  31089  nofulllem5  31105  ifscgr  31321  brsegle  31385  neibastop2lem  31525  curf  32557  finixpnum  32564  fin2solem  32565  fin2so  32566  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem14  32593  poimirlem16  32595  poimirlem19  32598  poimirlem22  32601  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimir  32612  heicant  32614  itg2gt0cn  32635  bddiblnc  32650  ftc1cnnc  32654  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anc  32663  cover2  32678  filbcmb  32705  fdc  32711  fdc1  32712  seqpo  32713  incsequz  32714  incsequz2  32715  metf1o  32721  lmclim2  32724  geomcau  32725  isbnd2  32752  bndss  32755  ismtybndlem  32775  heibor1lem  32778  rrncmslem  32801  rrnequiv  32804  exidreslem  32846  ghomco  32860  isdrngo3  32928  rngoisocnv  32950  isidlc  32984  idlnegcl  32991  divrngidl  32997  intidl  32998  unichnidl  33000  keridl  33001  igenmin  33033  prnc  33036  ispridlc  33039  prter3  33185  glbconxN  33682  atltcvr  33739  3dim1  33771  lvolnle3at  33886  linepsubN  34056  osumclN  34271  pexmidALTN  34282  lhpmatb  34335  cdlemg1idlemN  34878  dihlss  35557  dihglblem5aN  35599  dihatlat  35641  lsmfgcl  36662  kercvrlsm  36671  unxpwdom3  36683  hbt  36719  cntzsdrg  36791  cvgdvgrat  37534  climinf  38673  clim2f  38703  clim2cf  38717  clim0cf  38721  clim2f2  38737  fmtnofac2lem  40018  cusgrsize2inds  40669  mgmhmpropd  41575  mgmhmima  41592  ovmpt2rdxf  41910  cotsqcscsq  42302  aacllem  42356
  Copyright terms: Public domain W3C validator