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

Theorem anassrs 679
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 630 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 448 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  anass  680  mpanr1  718  pm2.61ddan  832  pm2.61dda  833  anass1rs  848  anabss5  856  anabss7  861  pm2.61da2ne  2879  ralimdvva  2961  2ralbida  2984  2ralbidva  2985  2rexbidva  3052  copsexg  4946  pofun  5041  imainss  5536  eqfnfv2  6298  fnex  6466  f1elima  6505  fliftfun  6547  isores2  6568  f1oiso  6586  ovmpt2dxf  6771  grpridd  6859  sorpssuni  6931  sorpssint  6932  tfindsg2  7046  oalim  7597  omlim  7598  oaass  7626  omlimcl  7643  omass  7645  oelim2  7660  oeoa  7662  oeoelem  7663  nnaass  7687  omabs  7712  eroveu  7827  sbthlem4  8058  fimaxg  8192  fisupg  8193  fofinf1o  8226  fiming  8389  fiinfg  8390  ordtypelem7  8414  hartogs  8434  card2on  8444  unwdomg  8474  wemapwe  8579  dfac5  8936  cfsmolem  9077  isf32lem2  9161  ttukeylem6  9321  ondomon  9370  alephreg  9389  ltexprlem6  9848  recexsrlem  9909  wloglei  10545  recextlem2  10643  fimaxre  10953  creur  10999  uz11  11695  xrmaxeq  11995  xrmineq  11996  xaddf  12040  xaddass  12064  xleadd1a  12068  xlt2add  12075  xmullem  12079  xmulgt0  12098  xmulasslem3  12101  xlemul1a  12103  xadddilem  12109  fzrevral  12409  seqcaopr2  12820  expnlbnd2  12978  faclbnd4lem4  13066  rtrclreclem3  13781  rtrclreclem4  13782  relexpindlem  13784  rtrclind  13786  shftlem  13789  01sqrex  13971  cau3lem  14075  limsupbnd2  14195  clim2  14216  clim2c  14217  clim0c  14219  rlimresb  14277  2clim  14284  climabs0  14297  climcn1  14303  climcn2  14304  o1rlimmul  14330  climsqz  14352  climsqz2  14353  rlimsqzlem  14360  lo1le  14363  climsup  14381  caucvgrlem2  14386  iseralt  14396  summolem2  14428  fsum2dlem  14482  cvgcmp  14529  cvgcmpce  14531  climfsum  14533  fsumiun  14534  geomulcvg  14588  mertenslem2  14598  mertens  14599  prodfn0  14607  prodfrec  14608  zprod  14648  fprodeq0  14686  fprodn0  14690  fprod2dlem  14691  smu01lem  15188  gcdcllem1  15202  gcdmultiplez  15251  dvdssq  15261  lcmgcdlem  15300  lcmdvds  15302  coprmdvds2  15349  pclem  15524  pcge0  15547  pcgcd1  15562  prmpwdvds  15589  1arithlem4  15611  4sqlem18  15647  vdwlem10  15675  vdwlem11  15676  ramval  15693  ramub1lem2  15712  ramcl  15714  imasaddfnlem  16169  imasaddflem  16171  imasvscafn  16178  imasleval  16182  ismon2  16375  isepi2  16382  issubc3  16490  cofucl  16529  setcmon  16718  setcepi  16719  ipodrsfi  17144  ipodrsima  17146  isacs3lem  17147  grpidpropd  17242  gsumpropd2lem  17254  mhmpropd  17322  mhmima  17344  gsumccat  17359  grplcan  17458  dfgrp3lem  17494  mulgdirlem  17553  subgmulg  17589  issubg4  17594  subgint  17599  cycsubgcl  17601  ssnmz  17617  gastacl  17723  orbsta  17727  cntzsubg  17750  galactghm  17804  odmulg  17954  odbezout  17956  sylow3lem2  18024  lsmsubm  18049  efgsfo  18133  mulgmhm  18214  mulgghm  18215  gsumval3  18289  gsumcllem  18290  gsumpt  18342  gsum2d  18352  gsum2d2  18354  prdsgsum  18358  subgdmdprd  18414  dprd2d2  18424  ablfac1eu  18453  srglmhm  18516  srgrmhm  18517  ringpropd  18563  ringlghm  18585  dvdsrpropd  18677  abvpropd  18823  islmodd  18850  lmodprop2d  18906  lsssubg  18938  lsspropd  18998  lmhmima  19028  lsmelval2  19066  lidlsubg  19196  assapropd  19308  asclpropd  19327  psrass1lem  19358  mplcoe1  19446  mplcoe5  19449  mplind  19483  evlslem2  19493  evlsval  19500  coe1tmmul2  19627  phlpropd  19981  frlmsslsp  20116  lindfmm  20147  islindf4  20158  mamuass  20189  mavmulass  20336  mdetuni0  20408  mdetmul  20410  cpmatacl  20502  cpmadugsumfi  20663  cpmadugsum  20664  cpmadumatpolylem1  20667  cpmadumatpolylem2  20668  cpmadumatpoly  20669  cayhamlem4  20674  neips  20898  neindisj  20902  ordtrest2lem  20988  lmbrf  21045  lmss  21083  isreg2  21162  lmmo  21165  hauscmplem  21190  bwth  21194  2ndcomap  21242  1stcelcls  21245  restlly  21267  islly2  21268  cldllycmp  21279  comppfsc  21316  1stckgenlem  21337  txbas  21351  txbasval  21390  tx1cn  21393  ptpjopn  21396  ptcnp  21406  txnlly  21421  txlm  21432  xkococn  21444  fgabs  21664  fmfnfmlem4  21742  flimcf  21767  hauspwpwf1  21772  fclsbas  21806  fclscf  21810  flimfnfcls  21813  ghmcnp  21899  tsmsxp  21939  isxmet2d  22113  elmopn2  22231  mopni3  22280  blsscls2  22290  metequiv2  22296  metss2lem  22297  met2ndci  22308  metrest  22310  metcnp  22327  metcnp2  22328  metcnpi3  22332  txmetcnp  22333  nmolb2d  22503  xrge0tsms  22618  metdsre  22637  metnrmlem3  22645  fsumcn  22654  elcncf2  22674  mulc1cncf  22689  cncfco  22691  cncfmet  22692  bndth  22738  evth  22739  copco  22799  pcopt2  22804  pcoass  22805  pcorevlem  22807  lmmcvg  23040  lmmbrf  23041  iscau4  23058  iscauf  23059  cmetcaulem  23067  iscmet3lem3  23069  iscmet3lem1  23070  causs  23077  equivcfil  23078  lmclim  23082  caubl  23087  caublcls  23088  bcth3  23109  ivthle  23206  ivthle2  23207  ovoliunlem1  23251  ovolicc2lem5  23270  volsuplem  23304  uniioombllem6  23337  dyaddisjlem  23344  dyadmax  23347  volcn  23355  mbfmulc2lem  23395  ismbf3d  23402  mbfsup  23412  mbfinf  23413  mbflim  23416  i1fmullem  23442  itg2seq  23490  itg2uba  23491  itg2splitlem  23496  itg2split  23497  itg2monolem1  23498  ditgsplitlem  23605  ellimc2  23622  ellimc3  23624  limcflf  23626  limcmpt  23628  limcco  23638  lhop1lem  23757  dvfsumle  23765  dvfsumabs  23767  dvfsumrlim  23775  ftc1a  23781  ftc1lem6  23785  mdegmullem  23819  elply2  23933  plypf1  23949  ulmcaulem  24129  ulmcau  24130  ulmss  24132  ulmdvlem3  24137  mtest  24139  itgulm  24143  abelthlem8  24174  abelth  24176  tanord  24265  cxpcn3lem  24469  mcubic  24555  cubic2  24556  dvdsflsumcom  24895  fsumdvdsmul  24902  lgsdchrval  25060  2sqlem9  25133  rplogsumlem2  25155  rpvmasumlem  25157  dchrvmasumlem1  25165  vmalogdivsum2  25208  logsqvma  25212  selberg  25218  selberg4  25231  pntibndlem3  25262  pntlem3  25279  pntleml  25281  padicabv  25300  padicabvf  25301  padicabvcxp  25302  ostth3  25308  axpasch  25802  axcontlem7  25831  axcontlem10  25834  cusgrsize2inds  26330  grpolcan  27354  nvmul0or  27475  nmosetre  27589  blocnilem  27629  blocni  27630  h2hcau  27806  h2hlm  27807  shsel3  28144  chscllem2  28467  homulcl  28588  adjsym  28662  cnvadj  28721  hhcno  28733  hhcnf  28734  lnopl  28743  unoplin  28749  counop  28750  lnfnl  28760  hmoplin  28771  hmopm  28850  nmcexi  28855  lnconi  28862  riesz3i  28891  leopmuli  28962  leopmul  28963  hstle  29059  mdsl0  29139  mdslmd1lem2  29155  atcvatlem  29214  chirredi  29223  cdj1i  29262  foresf1o  29315  isoun  29453  difioo  29518  xrge0tsmsd  29759  pstmxmet  29914  ordtrest2NEWlem  29942  esum2dlem  30128  esum2d  30129  dya2icoseg2  30314  eulerpartlemgc  30398  eulerpartlemgvv  30412  eulerpartlemgh  30414  eulerpartlemgs2  30416  ballotlemimin  30541  signstfvneq0  30623  hgt750lemb  30708  connpconn  31191  cvmliftmolem2  31238  cvmliftlem6  31246  cvmliftlem8  31248  cvmlift2lem10  31268  cvmlift2lem12  31270  elmrsubrn  31391  elintfv  31638  dfon2lem6  31667  poseq  31724  nosupbnd1lem5  31832  nocvxminlem  31867  ifscgr  32126  brsegle  32190  neibastop2lem  32330  curf  33358  finixpnum  33365  fin2solem  33366  fin2so  33367  lindsenlbs  33375  matunitlindflem1  33376  matunitlindflem2  33377  matunitlindf  33378  poimirlem3  33383  poimirlem4  33384  poimirlem6  33386  poimirlem7  33387  poimirlem14  33394  poimirlem16  33396  poimirlem19  33399  poimirlem22  33402  poimirlem28  33408  poimirlem29  33409  poimirlem30  33410  poimir  33413  heicant  33415  itg2gt0cn  33436  bddiblnc  33451  ftc1cnnc  33455  ftc1anclem5  33460  ftc1anclem6  33461  ftc1anclem7  33462  ftc1anc  33464  cover2  33479  filbcmb  33506  fdc  33512  fdc1  33513  seqpo  33514  incsequz  33515  incsequz2  33516  metf1o  33522  lmclim2  33525  geomcau  33526  isbnd2  33553  bndss  33556  ismtybndlem  33576  heibor1lem  33579  rrncmslem  33602  rrnequiv  33605  exidreslem  33647  ghomco  33661  isdrngo3  33729  rngoisocnv  33751  isidlc  33785  idlnegcl  33792  divrngidl  33798  intidl  33799  unichnidl  33801  keridl  33802  igenmin  33834  prnc  33837  ispridlc  33840  prter3  33986  glbconxN  34483  atltcvr  34540  3dim1  34572  lvolnle3at  34687  linepsubN  34857  osumclN  35072  pexmidALTN  35083  lhpmatb  35136  cdlemg1idlemN  35679  dihlss  36358  dihglblem5aN  36400  dihatlat  36442  lsmfgcl  37463  kercvrlsm  37472  unxpwdom3  37484  hbt  37519  cntzsdrg  37591  cvgdvgrat  38332  climinf  39638  clim2f  39668  clim2cf  39682  clim0cf  39686  clim2f2  39702  fmtnofac2lem  41245  mgmhmpropd  41550  mgmhmima  41567  ovmpt2rdxf  41882  cotsqcscsq  42268  aacllem  42312
  Copyright terms: Public domain W3C validator