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  3105  ralimdvva  3179  2ralbidva  3198  2ralbida  3232  reximdvva  3277  2rexbidva  3299  copsexgw  5373  copsexg  5374  pofun  5485  imainss  6005  eqfnfv2  6796  fnex  6972  f1elima  7012  fliftfun  7054  isores2  7075  f1oiso  7093  ovmpodxf  7289  sorpssuni  7447  sorpssint  7448  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  17862  grpridd  17875  gsumpropd2lem  17879  mhmpropd  17952  mhmima  17979  gsumccatOLD  17995  grplcan  18101  dfgrp3lem  18137  mulgdirlem  18198  subgmulg  18233  issubg4  18238  subgint  18243  ssnmz  18258  cycsubgcl  18289  gastacl  18379  orbsta  18383  cntzsubg  18407  galactghm  18463  odmulg  18614  odbezout  18616  sylow3lem2  18684  lsmsubm  18709  efgsfo  18796  mulgmhm  18879  mulgghm  18880  gsumval3  18958  gsumcllem  18959  gsumpt  19013  gsum2d  19023  gsum2d2  19025  prdsgsum  19032  subgdmdprd  19087  dprd2d2  19097  ablfac1eu  19126  srglmhm  19216  srgrmhm  19217  ringpropd  19263  ringlghm  19285  dvdsrpropd  19377  cntzsdrg  19512  abvpropd  19544  islmodd  19571  lmodprop2d  19627  lsssubg  19660  lsspropd  19720  lmhmima  19750  lidlsubg  19918  assapropd  20031  asclpropd  20056  psrass1lem  20087  mplcoe1  20176  mplcoe5  20179  mplind  20212  evlslem2  20222  evlsval  20229  coe1tmmul2  20374  phlpropd  20729  frlmsslsp  20870  lindfmm  20901  islindf4  20912  mamuass  20941  mavmulass  21088  mdetuni0  21160  mdetmul  21162  cpmatacl  21254  cpmadugsumfi  21415  cpmadumatpolylem1  21419  cpmadumatpolylem2  21420  cpmadumatpoly  21421  cayhamlem4  21426  neips  21651  neindisj  21655  ordtrest2lem  21741  lmbrf  21798  lmss  21836  isreg2  21915  lmmo  21918  hauscmplem  21944  bwth  21948  2ndcomap  21996  1stcelcls  21999  restlly  22021  islly2  22022  cldllycmp  22033  comppfsc  22070  1stckgenlem  22091  txbas  22105  txbasval  22144  tx1cn  22147  ptpjopn  22150  ptcnp  22160  txnlly  22175  txlm  22186  xkococn  22198  fgabs  22417  fmfnfmlem4  22495  flimcf  22520  hauspwpwf1  22525  fclsbas  22559  fclscf  22563  flimfnfcls  22566  ghmcnp  22652  tsmsxp  22692  isxmet2d  22866  elmopn2  22984  mopni3  23033  blsscls2  23043  metequiv2  23049  metss2lem  23050  met2ndci  23061  metrest  23063  metcnp  23080  metcnp2  23081  metcnpi3  23085  txmetcnp  23086  nmolb2d  23256  xrge0tsms  23371  metdsre  23390  metnrmlem3  23398  fsumcn  23407  elcncf2  23427  mulc1cncf  23442  cncfco  23444  cncfmet  23445  bndth  23491  evth  23492  copco  23551  pcopt2  23556  pcoass  23557  pcorevlem  23559  lmmcvg  23793  lmmbrf  23794  iscau4  23811  iscauf  23812  cmetcaulem  23820  iscmet3lem3  23822  iscmet3lem1  23823  causs  23830  equivcfil  23831  lmclim  23835  caubl  23840  caublcls  23841  bcth3  23863  ivthle  23986  ivthle2  23987  ovoliunlem1  24032  ovolicc2lem5  24051  volsuplem  24085  uniioombllem6  24118  dyaddisjlem  24125  dyadmax  24128  volcn  24136  mbfmulc2lem  24177  ismbf3d  24184  mbfsup  24194  mbfinf  24195  mbflim  24198  i1fmullem  24224  itg2seq  24272  itg2uba  24273  itg2splitlem  24278  itg2split  24279  itg2monolem1  24280  ditgsplitlem  24387  ellimc2  24404  ellimc3  24406  limcflf  24408  limcmpt  24410  limcco  24420  lhop1lem  24539  dvfsumle  24547  dvfsumabs  24549  dvfsumrlim  24557  ftc1a  24563  ftc1lem6  24567  mdegmullem  24601  elply2  24715  plypf1  24731  ulmcaulem  24911  ulmcau  24912  ulmss  24914  ulmdvlem3  24919  mtest  24921  itgulm  24925  abelthlem8  24956  abelth  24958  tanord  25049  cxpcn3lem  25255  mcubic  25352  cubic2  25353  dvdsflsumcom  25693  fsumdvdsmul  25700  lgsdchrval  25858  2sqlem9  25931  rplogsumlem2  25989  rpvmasumlem  25991  dchrvmasumlem1  25999  vmalogdivsum2  26042  logsqvma  26046  selberg  26052  selberg4  26065  pntibndlem3  26096  pntlem3  26113  pntleml  26115  padicabv  26134  padicabvf  26135  padicabvcxp  26136  ostth3  26142  axpasch  26655  axcontlem7  26684  axcontlem10  26687  cusgrsize2inds  27163  grpolcan  28235  nvmul0or  28355  nmosetre  28469  blocnilem  28509  blocni  28510  h2hcau  28684  h2hlm  28685  shsel3  29020  chscllem2  29343  homulcl  29464  adjsym  29538  cnvadj  29597  hhcno  29609  hhcnf  29610  lnopl  29619  unoplin  29625  counop  29626  lnfnl  29636  hmoplin  29647  hmopm  29726  nmcexi  29731  lnconi  29738  riesz3i  29767  leopmuli  29838  leopmul  29839  hstle  29935  mdsl0  30015  mdslmd1lem2  30031  atcvatlem  30090  chirredi  30099  cdj1i  30138  sbc2iedf  30158  foresf1o  30193  suppovss  30355  isoun  30364  difioo  30432  swrdf1  30558  xrge0tsmsd  30620  cycpmrn  30713  fedgmullem2  30926  pstmxmet  31037  ordtrest2NEWlem  31065  esum2dlem  31251  esum2d  31252  dya2icoseg2  31436  eulerpartlemgc  31520  eulerpartlemgh  31536  eulerpartlemgs2  31538  ballotlemimin  31663  signstfvneq0  31742  hgt750lemb  31827  connpconn  32380  cvmliftmolem2  32427  cvmliftlem6  32435  cvmliftlem8  32437  cvmlift2lem12  32459  elmrsubrn  32665  dfon2lem6  32931  poseq  32993  nosupbnd1lem5  33110  nocvxminlem  33145  ifscgr  33403  brsegle  33467  neibastop2lem  33606  curf  34752  finixpnum  34759  fin2solem  34760  fin2so  34761  lindsenlbs  34769  matunitlindflem1  34770  matunitlindflem2  34771  matunitlindf  34772  poimirlem3  34777  poimirlem4  34778  poimirlem6  34780  poimirlem7  34781  poimirlem14  34788  poimirlem16  34790  poimirlem19  34793  poimirlem22  34796  poimirlem28  34802  poimirlem29  34803  poimirlem30  34804  poimir  34807  heicant  34809  itg2gt0cn  34829  bddiblnc  34844  ftc1cnnc  34848  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anc  34857  cover2  34872  filbcmb  34898  fdc  34903  fdc1  34904  seqpo  34905  incsequz  34906  incsequz2  34907  metf1o  34913  lmclim2  34916  geomcau  34917  isbnd2  34944  bndss  34947  ismtybndlem  34967  heibor1lem  34970  rrncmslem  34993  rrnequiv  34996  exidreslem  35038  ghomco  35052  isdrngo3  35120  rngoisocnv  35142  isidlc  35176  idlnegcl  35183  divrngidl  35189  intidl  35190  unichnidl  35192  keridl  35193  igenmin  35225  prnc  35228  ispridlc  35231  erim2  35793  prter3  35900  glbconxN  36396  atltcvr  36453  3dim1  36485  lvolnle3at  36600  linepsubN  36770  osumclN  36985  pexmidALTN  36996  lhpmatb  37049  cdlemg1idlemN  37590  dihlss  38268  dihglblem5aN  38310  dihatlat  38352  prjspertr  39135  prjspreln0  39139  lsmfgcl  39554  kercvrlsm  39563  unxpwdom3  39575  hbt  39610  cvgdvgrat  40525  climinf  41767  clim2f  41797  clim2cf  41811  clim0cf  41815  clim2f2  41831  fmtnofac2lem  43577  isomuspgrlem2d  43843  mgmhmpropd  43899  mgmhmima  43916  ovmpordxf  44285  cotsqcscsq  44759  aacllem  44800
  Copyright terms: Public domain W3C validator