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

Theorem anassrs 677
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 628 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 446 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  anass  678  mpanr1  714  pm2.61ddan  828  pm2.61dda  829  anass1rs  844  anabss5  852  anabss7  857  pm2.61da2ne  2865  ralimdvva  2942  2ralbida  2965  2ralbidva  2966  2rexbidva  3033  copsexg  4872  pofun  4961  imainss  5449  eqfnfv2  6201  fnex  6360  f1elima  6395  fliftfun  6436  isores2  6457  f1oiso  6475  ovmpt2dxf  6658  grpridd  6745  sorpssuni  6817  sorpssint  6818  tfindsg2  6926  oalim  7472  omlim  7473  oaass  7501  omlimcl  7518  omass  7520  oelim2  7535  oeoa  7537  oeoelem  7538  nnaass  7562  omabs  7587  eroveu  7702  sbthlem4  7931  fimaxg  8065  fisupg  8066  fofinf1o  8099  fiming  8260  fiinfg  8261  ordtypelem7  8285  hartogs  8305  card2on  8315  unwdomg  8345  wemapwe  8450  dfac5  8807  cfsmolem  8948  isf32lem2  9032  ttukeylem6  9192  ondomon  9237  alephreg  9256  ltexprlem6  9715  recexsrlem  9776  wloglei  10405  recextlem2  10503  fimaxre  10813  creur  10857  uz11  11538  xrmaxeq  11839  xrmineq  11840  xaddf  11884  xaddass  11904  xleadd1a  11908  xlt2add  11915  xmullem  11919  xmulgt0  11938  xmulasslem3  11941  xlemul1a  11943  xadddilem  11949  fzrevral  12245  seqcaopr2  12650  expnlbnd2  12808  faclbnd4lem4  12896  rtrclreclem3  13590  rtrclreclem4  13591  relexpindlem  13593  rtrclind  13595  shftlem  13598  01sqrex  13780  cau3lem  13884  limsupbnd2  14004  clim2  14025  clim2c  14026  clim0c  14028  rlimresb  14086  2clim  14093  climabs0  14106  climcn1  14112  climcn2  14113  o1rlimmul  14139  climsqz  14161  climsqz2  14162  rlimsqzlem  14169  lo1le  14172  climsup  14190  caucvgrlem2  14195  iseralt  14205  summolem2  14236  fsum2dlem  14285  cvgcmp  14331  cvgcmpce  14333  climfsum  14335  fsumiun  14336  geomulcvg  14388  mertenslem2  14398  mertens  14399  prodfn0  14407  prodfrec  14408  zprod  14448  fprodeq0  14486  fprodn0  14490  fprod2dlem  14491  smu01lem  14987  gcdcllem1  15001  gcdmultiplez  15050  dvdssq  15060  lcmgcdlem  15099  lcmdvds  15101  coprmdvds2  15148  pclem  15323  pcge0  15346  pcgcd1  15361  prmpwdvds  15388  1arithlem4  15410  4sqlem18  15446  vdwlem10  15474  vdwlem11  15475  ramval  15492  ramub1lem2  15511  ramcl  15513  imasaddfnlem  15953  imasaddflem  15955  imasvscafn  15962  imasleval  15966  ismon2  16159  isepi2  16166  issubc3  16274  cofucl  16313  setcmon  16502  setcepi  16503  ipodrsfi  16928  ipodrsima  16930  isacs3lem  16931  grpidpropd  17026  gsumpropd2lem  17038  mhmpropd  17106  mhmima  17128  gsumccat  17143  grplcan  17242  dfgrp3lem  17278  mulgdirlem  17337  subgmulg  17373  issubg4  17378  subgint  17383  cycsubgcl  17385  ssnmz  17401  gastacl  17507  orbsta  17511  cntzsubg  17534  galactghm  17588  odmulg  17738  odbezout  17740  sylow3lem2  17808  lsmsubm  17833  efgsfo  17917  mulgmhm  17998  mulgghm  17999  gsumval3  18073  gsumcllem  18074  gsumpt  18126  gsum2d  18136  gsum2d2  18138  prdsgsum  18142  subgdmdprd  18198  dprd2d2  18208  ablfac1eu  18237  srglmhm  18300  srgrmhm  18301  ringpropd  18347  ringlghm  18369  dvdsrpropd  18461  abvpropd  18607  islmodd  18634  lmodprop2d  18690  lsssubg  18720  lsspropd  18780  lmhmima  18810  lsmelval2  18848  lidlsubg  18978  assapropd  19090  asclpropd  19109  psrass1lem  19140  mplcoe1  19228  mplcoe5  19231  mplind  19265  evlslem2  19275  evlsval  19282  coe1tmmul2  19409  phlpropd  19760  frlmsslsp  19892  lindfmm  19923  islindf4  19934  mamuass  19965  mavmulass  20112  mdetuni0  20184  mdetmul  20186  cpmatacl  20278  cpmadugsumfi  20439  cpmadugsum  20440  cpmadumatpolylem1  20443  cpmadumatpolylem2  20444  cpmadumatpoly  20445  cayhamlem4  20450  neips  20665  neindisj  20669  ordtrest2lem  20755  lmbrf  20812  lmss  20850  isreg2  20929  lmmo  20932  hauscmplem  20957  bwth  20961  2ndcomap  21009  1stcelcls  21012  restlly  21034  islly2  21035  cldllycmp  21046  comppfsc  21083  1stckgenlem  21104  txbas  21118  txbasval  21157  tx1cn  21160  ptpjopn  21163  ptcnp  21173  txnlly  21188  txlm  21199  xkococn  21211  fgabs  21431  fmfnfmlem4  21509  flimcf  21534  hauspwpwf1  21539  fclsbas  21573  fclscf  21577  flimfnfcls  21580  ghmcnp  21666  tsmsxp  21706  isxmet2d  21879  elmopn2  21997  mopni3  22046  blsscls2  22056  metequiv2  22062  metss2lem  22063  met2ndci  22074  metrest  22076  metcnp  22093  metcnp2  22094  metcnpi3  22098  txmetcnp  22099  nmolb2d  22260  xrge0tsms  22373  metdsre  22391  metnrmlem3  22399  fsumcn  22408  elcncf2  22428  mulc1cncf  22443  cncfco  22445  cncfmet  22446  bndth  22492  evth  22493  copco  22553  pcopt2  22558  pcoass  22559  pcorevlem  22561  lmmcvg  22781  lmmbrf  22782  iscau4  22799  iscauf  22800  cmetcaulem  22808  iscmet3lem3  22810  iscmet3lem1  22811  causs  22818  equivcfil  22819  lmclim  22822  caubl  22827  caublcls  22828  bcth3  22849  ivthle  22945  ivthle2  22946  ovoliunlem1  22990  ovolicc2lem5  23009  volsuplem  23043  uniioombllem6  23075  dyaddisjlem  23082  dyadmax  23085  volcn  23093  mbfmulc2lem  23133  ismbf3d  23140  mbfsup  23150  mbfinf  23151  mbflim  23154  i1fmullem  23180  itg2seq  23228  itg2uba  23229  itg2splitlem  23234  itg2split  23235  itg2monolem1  23236  ditgsplitlem  23343  ellimc2  23360  ellimc3  23362  limcflf  23364  limcmpt  23366  limcco  23376  lhop1lem  23493  dvfsumle  23501  dvfsumabs  23503  dvfsumrlim  23511  ftc1a  23517  ftc1lem6  23521  mdegmullem  23555  elply2  23669  plypf1  23685  ulmcaulem  23865  ulmcau  23866  ulmss  23868  ulmdvlem3  23873  mtest  23875  itgulm  23879  abelthlem8  23910  abelth  23912  tanord  24001  cxpcn3lem  24201  mcubic  24287  cubic2  24288  dvdsflsumcom  24627  fsumdvdsmul  24634  lgsdchrval  24792  2sqlem9  24865  rplogsumlem2  24887  rpvmasumlem  24889  dchrvmasumlem1  24897  vmalogdivsum2  24940  logsqvma  24944  selberg  24950  selberg4  24963  pntibndlem3  24994  pntlem3  25011  pntleml  25013  padicabv  25032  padicabvf  25033  padicabvcxp  25034  ostth3  25040  axpasch  25535  axcontlem7  25564  axcontlem10  25567  cusgrasize2inds  25767  2spotdisj  26350  grpolcan  26530  nvmul0or  26673  sspival  26777  nmosetre  26805  blocnilem  26845  blocni  26846  h2hcau  27022  h2hlm  27023  shsel3  27360  chscllem2  27683  homulcl  27804  adjsym  27878  cnvadj  27937  hhcno  27949  hhcnf  27950  lnopl  27959  unoplin  27965  counop  27966  lnfnl  27976  hmoplin  27987  hmopm  28066  nmcexi  28071  lnconi  28078  riesz3i  28107  leopmuli  28178  leopmul  28179  hstle  28275  mdsl0  28355  mdslmd1lem2  28371  atcvatlem  28430  chirredi  28439  cdj1i  28478  foresf1o  28529  isoun  28664  difioo  28736  xrge0tsmsd  28918  pstmxmet  29070  ordtrest2NEWlem  29098  esum2dlem  29283  esum2d  29284  dya2icoseg2  29469  eulerpartlemgc  29553  eulerpartlemgvv  29567  eulerpartlemgh  29569  eulerpartlemgs2  29571  ballotlemimin  29696  signstfvneq0  29777  conpcon  30273  cvmliftmolem2  30320  cvmliftlem6  30328  cvmliftlem8  30330  cvmlift2lem10  30350  cvmlift2lem12  30352  elmrsubrn  30473  dfon2lem6  30739  poseq  30796  nocvxminlem  30891  nofulllem5  30907  ifscgr  31123  brsegle  31187  neibastop2lem  31327  curf  32356  finixpnum  32363  fin2solem  32364  fin2so  32365  lindsenlbs  32373  matunitlindflem1  32374  matunitlindflem2  32375  matunitlindf  32376  poimirlem3  32381  poimirlem4  32382  poimirlem6  32384  poimirlem7  32385  poimirlem14  32392  poimirlem16  32394  poimirlem19  32397  poimirlem22  32400  poimirlem28  32406  poimirlem29  32407  poimirlem30  32408  poimir  32411  heicant  32413  itg2gt0cn  32434  bddiblnc  32449  ftc1cnnc  32453  ftc1anclem5  32458  ftc1anclem6  32459  ftc1anclem7  32460  ftc1anc  32462  cover2  32477  filbcmb  32504  fdc  32510  fdc1  32511  seqpo  32512  incsequz  32513  incsequz2  32514  metf1o  32520  lmclim2  32523  geomcau  32524  isbnd2  32551  bndss  32554  ismtybndlem  32574  heibor1lem  32577  rrncmslem  32600  rrnequiv  32603  exidreslem  32645  ghomco  32659  isdrngo3  32727  rngoisocnv  32749  isidlc  32783  idlnegcl  32790  divrngidl  32796  intidl  32797  unichnidl  32799  keridl  32800  igenmin  32832  prnc  32835  ispridlc  32838  prter3  32984  glbconxN  33481  atltcvr  33538  3dim1  33570  lvolnle3at  33685  linepsubN  33855  osumclN  34070  pexmidALTN  34081  lhpmatb  34134  cdlemg1idlemN  34677  dihlss  35356  dihglblem5aN  35398  dihatlat  35440  lsmfgcl  36461  kercvrlsm  36470  unxpwdom3  36482  hbt  36518  cntzsdrg  36590  cvgdvgrat  37333  climinf  38473  clim2f  38503  clim2cf  38517  clim0cf  38521  clim2f2  38537  fmtnofac2lem  39819  cusgrsize2inds  40667  mgmhmpropd  41573  mgmhmima  41590  ovmpt2rdxf  41908  cotsqcscsq  42261  aacllem  42315
  Copyright terms: Public domain W3C validator