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

Theorem anassrs 468
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 421 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 418 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  anass  469  anass1rs  651  anabss5  664  anabss7  669  mpanr1  699  pm2.61ddan  810  pm2.61dda  811  pm2.61da2ne  3110  ralimdvva  3184  2ralbidva  3203  2ralbida  3237  reximdvva  3282  2rexbidva  3304  copsexgw  5378  copsexg  5379  pofun  5490  imainss  6009  eqfnfv2  6799  fnex  6975  f1elima  7015  fliftfun  7057  isores2  7078  f1oiso  7096  ovmpodxf  7290  sorpssuni  7448  sorpssint  7449  tfindsg2  7564  2ndconst  7787  oalim  8148  omlim  8149  oaass  8177  omlimcl  8194  omass  8196  oelim2  8211  oeoa  8213  oeoelem  8214  nnaass  8238  omabs  8264  eroveu  8382  sbthlem4  8619  fimaxg  8754  fisupg  8755  fofinf1o  8788  fiming  8951  fiinfg  8952  ordtypelem7  8977  hartogs  8997  card2on  9007  unwdomg  9037  wemapwe  9149  dfac5  9543  cfsmolem  9681  isf32lem2  9765  ttukeylem6  9925  ondomon  9974  alephreg  9993  ltexprlem6  10452  recexsrlem  10514  wloglei  11161  recextlem2  11260  fimaxre  11573  fimaxreOLD  11574  creur  11621  uz11  12256  xrmaxeq  12562  xrmineq  12563  xaddf  12607  xaddass  12632  xleadd1a  12636  xlt2add  12643  xmullem  12647  xmulgt0  12666  xmulasslem3  12669  xlemul1a  12671  xadddilem  12677  fzrevral  12982  seqcaopr2  13396  expnlbnd2  13585  faclbnd4lem4  13646  hashgt23el  13775  rtrclreclem3  14409  rtrclreclem4  14410  relexpindlem  14412  rtrclind  14414  shftlem  14417  01sqrex  14599  cau3lem  14704  limsupbnd2  14830  clim2  14851  clim2c  14852  clim0c  14854  rlimresb  14912  2clim  14919  climabs0  14932  climcn1  14938  climcn2  14939  o1rlimmul  14965  climsqz  14987  climsqz2  14988  rlimsqzlem  14995  lo1le  14998  climsup  15016  caucvgrlem2  15021  iseralt  15031  summolem2  15063  fsum2dlem  15115  cvgcmp  15161  cvgcmpce  15163  climfsum  15165  fsumiun  15166  geomulcvg  15222  mertenslem2  15231  mertens  15232  prodfn0  15240  prodfrec  15241  zprod  15281  fprodeq0  15319  fprodn0  15323  fprod2dlem  15324  smu01lem  15824  gcdcllem1  15838  gcdmultiplezOLD  15891  dvdssq  15901  lcmdvds  15942  coprmdvds2  15988  pclem  16165  pcge0  16188  pcgcd1  16203  prmpwdvds  16230  1arithlem4  16252  4sqlem18  16288  vdwlem10  16316  vdwlem11  16317  ramval  16334  ramub1lem2  16353  ramcl  16355  imasaddfnlem  16791  imasaddflem  16793  imasvscafn  16800  imasleval  16804  ismon2  16994  isepi2  17001  issubc3  17109  cofucl  17148  setcmon  17337  setcepi  17338  ipodrsfi  17763  ipodrsima  17765  isacs3lem  17766  grpidpropd  17861  grpridd  17874  gsumpropd2lem  17878  mhmpropd  17950  mhmima  17972  gsumccatOLD  17988  grplcan  18091  dfgrp3lem  18127  mulgdirlem  18188  subgmulg  18223  issubg4  18228  subgint  18233  ssnmz  18248  cycsubgcl  18279  gastacl  18369  orbsta  18373  cntzsubg  18397  galactghm  18451  odmulg  18603  odbezout  18605  sylow3lem2  18673  lsmsubm  18698  efgsfo  18785  mulgmhm  18868  mulgghm  18869  gsumval3  18947  gsumcllem  18948  gsumpt  19002  gsum2d  19012  gsum2d2  19014  prdsgsum  19021  subgdmdprd  19076  dprd2d2  19086  ablfac1eu  19115  srglmhm  19205  srgrmhm  19206  ringpropd  19252  ringlghm  19274  dvdsrpropd  19366  cntzsdrg  19501  abvpropd  19533  islmodd  19560  lmodprop2d  19616  lsssubg  19649  lsspropd  19709  lmhmima  19739  lidlsubg  19907  assapropd  20020  asclpropd  20045  psrass1lem  20076  mplcoe1  20164  mplcoe5  20167  mplind  20200  evlslem2  20210  evlsval  20217  coe1tmmul2  20361  phlpropd  20715  frlmsslsp  20856  lindfmm  20887  islindf4  20898  mamuass  20927  mavmulass  21074  mdetuni0  21146  mdetmul  21148  cpmatacl  21240  cpmadugsumfi  21401  cpmadumatpolylem1  21405  cpmadumatpolylem2  21406  cpmadumatpoly  21407  cayhamlem4  21412  neips  21637  neindisj  21641  ordtrest2lem  21727  lmbrf  21784  lmss  21822  isreg2  21901  lmmo  21904  hauscmplem  21930  bwth  21934  2ndcomap  21982  1stcelcls  21985  restlly  22007  islly2  22008  cldllycmp  22019  comppfsc  22056  1stckgenlem  22077  txbas  22091  txbasval  22130  tx1cn  22133  ptpjopn  22136  ptcnp  22146  txnlly  22161  txlm  22172  xkococn  22184  fgabs  22403  fmfnfmlem4  22481  flimcf  22506  hauspwpwf1  22511  fclsbas  22545  fclscf  22549  flimfnfcls  22552  ghmcnp  22638  tsmsxp  22678  isxmet2d  22852  elmopn2  22970  mopni3  23019  blsscls2  23029  metequiv2  23035  metss2lem  23036  met2ndci  23047  metrest  23049  metcnp  23066  metcnp2  23067  metcnpi3  23071  txmetcnp  23072  nmolb2d  23242  xrge0tsms  23357  metdsre  23376  metnrmlem3  23384  fsumcn  23393  elcncf2  23413  mulc1cncf  23428  cncfco  23430  cncfmet  23431  bndth  23477  evth  23478  copco  23537  pcopt2  23542  pcoass  23543  pcorevlem  23545  lmmcvg  23779  lmmbrf  23780  iscau4  23797  iscauf  23798  cmetcaulem  23806  iscmet3lem3  23808  iscmet3lem1  23809  causs  23816  equivcfil  23817  lmclim  23821  caubl  23826  caublcls  23827  bcth3  23849  ivthle  23972  ivthle2  23973  ovoliunlem1  24018  ovolicc2lem5  24037  volsuplem  24071  uniioombllem6  24104  dyaddisjlem  24111  dyadmax  24114  volcn  24122  mbfmulc2lem  24163  ismbf3d  24170  mbfsup  24180  mbfinf  24181  mbflim  24184  i1fmullem  24210  itg2seq  24258  itg2uba  24259  itg2splitlem  24264  itg2split  24265  itg2monolem1  24266  ditgsplitlem  24373  ellimc2  24390  ellimc3  24392  limcflf  24394  limcmpt  24396  limcco  24406  lhop1lem  24525  dvfsumle  24533  dvfsumabs  24535  dvfsumrlim  24543  ftc1a  24549  ftc1lem6  24553  mdegmullem  24587  elply2  24701  plypf1  24717  ulmcaulem  24897  ulmcau  24898  ulmss  24900  ulmdvlem3  24905  mtest  24907  itgulm  24911  abelthlem8  24942  abelth  24944  tanord  25035  cxpcn3lem  25241  mcubic  25338  cubic2  25339  dvdsflsumcom  25679  fsumdvdsmul  25686  lgsdchrval  25844  2sqlem9  25917  rplogsumlem2  25975  rpvmasumlem  25977  dchrvmasumlem1  25985  vmalogdivsum2  26028  logsqvma  26032  selberg  26038  selberg4  26051  pntibndlem3  26082  pntlem3  26099  pntleml  26101  padicabv  26120  padicabvf  26121  padicabvcxp  26122  ostth3  26128  axpasch  26641  axcontlem7  26670  axcontlem10  26673  cusgrsize2inds  27149  grpolcan  28221  nvmul0or  28341  nmosetre  28455  blocnilem  28495  blocni  28496  h2hcau  28670  h2hlm  28671  shsel3  29006  chscllem2  29329  homulcl  29450  adjsym  29524  cnvadj  29583  hhcno  29595  hhcnf  29596  lnopl  29605  unoplin  29611  counop  29612  lnfnl  29622  hmoplin  29633  hmopm  29712  nmcexi  29717  lnconi  29724  riesz3i  29753  leopmuli  29824  leopmul  29825  hstle  29921  mdsl0  30001  mdslmd1lem2  30017  atcvatlem  30076  chirredi  30085  cdj1i  30124  sbc2iedf  30144  foresf1o  30179  suppovss  30341  isoun  30350  difioo  30418  swrdf1  30544  xrge0tsmsd  30606  cycpmrn  30699  fedgmullem2  30912  pstmxmet  31023  ordtrest2NEWlem  31051  esum2dlem  31237  esum2d  31238  dya2icoseg2  31422  eulerpartlemgc  31506  eulerpartlemgh  31522  eulerpartlemgs2  31524  ballotlemimin  31649  signstfvneq0  31728  hgt750lemb  31813  connpconn  32366  cvmliftmolem2  32413  cvmliftlem6  32421  cvmliftlem8  32423  cvmlift2lem12  32445  elmrsubrn  32651  dfon2lem6  32917  poseq  32979  nosupbnd1lem5  33096  nocvxminlem  33131  ifscgr  33389  brsegle  33453  neibastop2lem  33592  curf  34737  finixpnum  34744  fin2solem  34745  fin2so  34746  lindsenlbs  34754  matunitlindflem1  34755  matunitlindflem2  34756  matunitlindf  34757  poimirlem3  34762  poimirlem4  34763  poimirlem6  34765  poimirlem7  34766  poimirlem14  34773  poimirlem16  34775  poimirlem19  34778  poimirlem22  34781  poimirlem28  34787  poimirlem29  34788  poimirlem30  34789  poimir  34792  heicant  34794  itg2gt0cn  34814  bddiblnc  34829  ftc1cnnc  34833  ftc1anclem5  34838  ftc1anclem6  34839  ftc1anclem7  34840  ftc1anc  34842  cover2  34857  filbcmb  34883  fdc  34888  fdc1  34889  seqpo  34890  incsequz  34891  incsequz2  34892  metf1o  34898  lmclim2  34901  geomcau  34902  isbnd2  34929  bndss  34932  ismtybndlem  34952  heibor1lem  34955  rrncmslem  34978  rrnequiv  34981  exidreslem  35023  ghomco  35037  isdrngo3  35105  rngoisocnv  35127  isidlc  35161  idlnegcl  35168  divrngidl  35174  intidl  35175  unichnidl  35177  keridl  35178  igenmin  35210  prnc  35213  ispridlc  35216  erim2  35778  prter3  35885  glbconxN  36381  atltcvr  36438  3dim1  36470  lvolnle3at  36585  linepsubN  36755  osumclN  36970  pexmidALTN  36981  lhpmatb  37034  cdlemg1idlemN  37575  dihlss  38253  dihglblem5aN  38295  dihatlat  38337  prjspertr  39120  prjspreln0  39124  lsmfgcl  39539  kercvrlsm  39548  unxpwdom3  39560  hbt  39595  cvgdvgrat  40510  climinf  41752  clim2f  41782  clim2cf  41796  clim0cf  41800  clim2f2  41816  fmtnofac2lem  43562  isomuspgrlem2d  43828  mgmhmpropd  43884  mgmhmima  43901  ovmpordxf  44219  cotsqcscsq  44693  aacllem  44734
  Copyright terms: Public domain W3C validator