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

Theorem anassrs 455
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 409 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 406 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 198  df-an 385
This theorem is referenced by:  anass  456  anass1rs  637  anabss5  650  anabss7  655  mpanr1  686  pm2.61ddan  839  pm2.61dda  840  pm2.61da2ne  3077  ralimdvva  3163  2ralbida  3186  2ralbidva  3187  reximdvva  3218  2rexbidva  3255  copsexg  5158  pofun  5261  imainss  5773  eqfnfv2  6544  fnex  6716  f1elima  6754  fliftfun  6796  isores2  6817  f1oiso  6835  ovmpt2dxf  7026  grpridd  7114  sorpssuni  7186  sorpssint  7187  tfindsg2  7301  oalim  7859  omlim  7860  oaass  7888  omlimcl  7905  omass  7907  oelim2  7922  oeoa  7924  oeoelem  7925  nnaass  7949  omabs  7974  eroveu  8088  sbthlem4  8322  fimaxg  8456  fisupg  8457  fofinf1o  8490  fiming  8653  fiinfg  8654  ordtypelem7  8678  hartogs  8698  card2on  8708  unwdomg  8738  wemapwe  8851  dfac5  9244  cfsmolem  9387  isf32lem2  9471  ttukeylem6  9631  ondomon  9680  alephreg  9699  ltexprlem6  10158  recexsrlem  10219  wloglei  10855  recextlem2  10953  fimaxre  11263  creur  11309  uz11  11947  xrmaxeq  12248  xrmineq  12249  xaddf  12293  xaddass  12317  xleadd1a  12321  xlt2add  12328  xmullem  12332  xmulgt0  12351  xmulasslem3  12354  xlemul1a  12356  xadddilem  12362  fzrevral  12668  seqcaopr2  13080  expnlbnd2  13238  faclbnd4lem4  13323  rtrclreclem3  14043  rtrclreclem4  14044  relexpindlem  14046  rtrclind  14048  shftlem  14051  01sqrex  14233  cau3lem  14337  limsupbnd2  14457  clim2  14478  clim2c  14479  clim0c  14481  rlimresb  14539  2clim  14546  climabs0  14559  climcn1  14565  climcn2  14566  o1rlimmul  14592  climsqz  14614  climsqz2  14615  rlimsqzlem  14622  lo1le  14625  climsup  14643  caucvgrlem2  14648  iseralt  14658  summolem2  14690  fsum2dlem  14744  cvgcmp  14790  cvgcmpce  14792  climfsum  14794  fsumiun  14795  geomulcvg  14849  mertenslem2  14858  mertens  14859  prodfn0  14867  prodfrec  14868  zprod  14908  fprodeq0  14946  fprodn0  14950  fprod2dlem  14951  smu01lem  15446  gcdcllem1  15460  gcdmultiplez  15509  dvdssq  15519  lcmdvds  15560  coprmdvds2  15606  pclem  15780  pcge0  15803  pcgcd1  15818  prmpwdvds  15845  1arithlem4  15867  4sqlem18  15903  vdwlem10  15931  vdwlem11  15932  ramval  15949  ramub1lem2  15968  ramcl  15970  imasaddfnlem  16413  imasaddflem  16415  imasvscafn  16422  imasleval  16426  ismon2  16618  isepi2  16625  issubc3  16733  cofucl  16772  setcmon  16961  setcepi  16962  ipodrsfi  17388  ipodrsima  17390  isacs3lem  17391  grpidpropd  17486  gsumpropd2lem  17498  mhmpropd  17566  mhmima  17588  gsumccat  17603  grplcan  17702  dfgrp3lem  17738  mulgdirlem  17795  subgmulg  17830  issubg4  17835  subgint  17840  cycsubgcl  17842  ssnmz  17858  gastacl  17963  orbsta  17967  cntzsubg  17990  galactghm  18044  odmulg  18194  odbezout  18196  sylow3lem2  18264  lsmsubm  18289  efgsfo  18373  mulgmhm  18454  mulgghm  18455  gsumval3  18529  gsumcllem  18530  gsumpt  18582  gsum2d  18592  gsum2d2  18594  prdsgsum  18598  subgdmdprd  18655  dprd2d2  18665  ablfac1eu  18694  srglmhm  18757  srgrmhm  18758  ringpropd  18804  ringlghm  18826  dvdsrpropd  18918  abvpropd  19066  islmodd  19093  lmodprop2d  19149  lsssubg  19184  lsspropd  19244  lmhmima  19274  lidlsubg  19444  assapropd  19556  asclpropd  19575  psrass1lem  19606  mplcoe1  19694  mplcoe5  19697  mplind  19730  evlslem2  19740  evlsval  19747  coe1tmmul2  19874  phlpropd  20230  frlmsslsp  20366  lindfmm  20397  islindf4  20408  mamuass  20439  mavmulass  20587  mdetuni0  20659  mdetmul  20661  cpmatacl  20755  cpmadugsumfi  20916  cpmadumatpolylem1  20920  cpmadumatpolylem2  20921  cpmadumatpoly  20922  cayhamlem4  20927  neips  21152  neindisj  21156  ordtrest2lem  21242  lmbrf  21299  lmss  21337  isreg2  21416  lmmo  21419  hauscmplem  21444  bwth  21448  2ndcomap  21496  1stcelcls  21499  restlly  21521  islly2  21522  cldllycmp  21533  comppfsc  21570  1stckgenlem  21591  txbas  21605  txbasval  21644  tx1cn  21647  ptpjopn  21650  ptcnp  21660  txnlly  21675  txlm  21686  xkococn  21698  fgabs  21917  fmfnfmlem4  21995  flimcf  22020  hauspwpwf1  22025  fclsbas  22059  fclscf  22063  flimfnfcls  22066  ghmcnp  22152  tsmsxp  22192  isxmet2d  22366  elmopn2  22484  mopni3  22533  blsscls2  22543  metequiv2  22549  metss2lem  22550  met2ndci  22561  metrest  22563  metcnp  22580  metcnp2  22581  metcnpi3  22585  txmetcnp  22586  nmolb2d  22756  xrge0tsms  22871  metdsre  22890  metnrmlem3  22898  fsumcn  22907  elcncf2  22927  mulc1cncf  22942  cncfco  22944  cncfmet  22945  bndth  22991  evth  22992  copco  23051  pcopt2  23056  pcoass  23057  pcorevlem  23059  lmmcvg  23293  lmmbrf  23294  iscau4  23311  iscauf  23312  cmetcaulem  23320  iscmet3lem3  23322  iscmet3lem1  23323  causs  23330  equivcfil  23331  lmclim  23335  caubl  23340  caublcls  23341  bcth3  23362  ivthle  23460  ivthle2  23461  ovoliunlem1  23506  ovolicc2lem5  23525  volsuplem  23559  uniioombllem6  23592  dyaddisjlem  23599  dyadmax  23602  volcn  23610  mbfmulc2lem  23651  ismbf3d  23658  mbfsup  23668  mbfinf  23669  mbflim  23672  i1fmullem  23698  itg2seq  23746  itg2uba  23747  itg2splitlem  23752  itg2split  23753  itg2monolem1  23754  ditgsplitlem  23861  ellimc2  23878  ellimc3  23880  limcflf  23882  limcmpt  23884  limcco  23894  lhop1lem  24013  dvfsumle  24021  dvfsumabs  24023  dvfsumrlim  24031  ftc1a  24037  ftc1lem6  24041  mdegmullem  24075  elply2  24189  plypf1  24205  ulmcaulem  24385  ulmcau  24386  ulmss  24388  ulmdvlem3  24393  mtest  24395  itgulm  24399  abelthlem8  24430  abelth  24432  tanord  24522  cxpcn3lem  24725  mcubic  24811  cubic2  24812  dvdsflsumcom  25151  fsumdvdsmul  25158  lgsdchrval  25316  2sqlem9  25389  rplogsumlem2  25411  rpvmasumlem  25413  dchrvmasumlem1  25421  vmalogdivsum2  25464  logsqvma  25468  selberg  25474  selberg4  25487  pntibndlem3  25518  pntlem3  25535  pntleml  25537  padicabv  25556  padicabvf  25557  padicabvcxp  25558  ostth3  25564  axpasch  26058  axcontlem7  26087  axcontlem10  26090  cusgrsize2inds  26600  grpolcan  27736  nvmul0or  27856  nmosetre  27970  blocnilem  28010  blocni  28011  h2hcau  28187  h2hlm  28188  shsel3  28525  chscllem2  28848  homulcl  28969  adjsym  29043  cnvadj  29102  hhcno  29114  hhcnf  29115  lnopl  29124  unoplin  29130  counop  29131  lnfnl  29141  hmoplin  29152  hmopm  29231  nmcexi  29236  lnconi  29243  riesz3i  29272  leopmuli  29343  leopmul  29344  hstle  29440  mdsl0  29520  mdslmd1lem2  29536  atcvatlem  29595  chirredi  29604  cdj1i  29643  foresf1o  29691  isoun  29829  difioo  29894  xrge0tsmsd  30133  pstmxmet  30288  ordtrest2NEWlem  30316  esum2dlem  30502  esum2d  30503  dya2icoseg2  30688  eulerpartlemgc  30772  eulerpartlemgh  30788  eulerpartlemgs2  30790  ballotlemimin  30915  signstfvneq0  30997  hgt750lemb  31082  connpconn  31562  cvmliftmolem2  31609  cvmliftlem6  31617  cvmliftlem8  31619  cvmlift2lem12  31641  elmrsubrn  31762  elintfv  32006  dfon2lem6  32035  poseq  32096  nosupbnd1lem5  32201  nocvxminlem  32236  ifscgr  32494  brsegle  32558  neibastop2lem  32698  curf  33719  finixpnum  33726  fin2solem  33727  fin2so  33728  lindsenlbs  33736  matunitlindflem1  33737  matunitlindflem2  33738  matunitlindf  33739  poimirlem3  33744  poimirlem4  33745  poimirlem6  33747  poimirlem7  33748  poimirlem14  33755  poimirlem16  33757  poimirlem19  33760  poimirlem22  33763  poimirlem28  33769  poimirlem29  33770  poimirlem30  33771  poimir  33774  heicant  33776  itg2gt0cn  33796  bddiblnc  33811  ftc1cnnc  33815  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem7  33822  ftc1anc  33824  cover2  33839  filbcmb  33866  fdc  33871  fdc1  33872  seqpo  33873  incsequz  33874  incsequz2  33875  metf1o  33881  lmclim2  33884  geomcau  33885  isbnd2  33912  bndss  33915  ismtybndlem  33935  heibor1lem  33938  rrncmslem  33961  rrnequiv  33964  exidreslem  34006  ghomco  34020  isdrngo3  34088  rngoisocnv  34110  isidlc  34144  idlnegcl  34151  divrngidl  34157  intidl  34158  unichnidl  34160  keridl  34161  igenmin  34193  prnc  34196  ispridlc  34199  prter3  34680  glbconxN  35177  atltcvr  35234  3dim1  35266  lvolnle3at  35381  linepsubN  35551  osumclN  35766  pexmidALTN  35777  lhpmatb  35830  cdlemg1idlemN  36371  dihlss  37049  dihglblem5aN  37091  dihatlat  37133  lsmfgcl  38163  kercvrlsm  38172  unxpwdom3  38184  hbt  38219  cntzsdrg  38291  cvgdvgrat  39030  climinf  40336  clim2f  40366  clim2cf  40380  clim0cf  40384  clim2f2  40400  fmtnofac2lem  42073  mgmhmpropd  42371  mgmhmima  42388  ovmpt2rdxf  42703  cotsqcscsq  43092  aacllem  43136
  Copyright terms: Public domain W3C validator