Theorem anassrs 467

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

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 417	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anass  468  anass1rs  656  anabss5  669  anabss7  674  mpanr1  704  pm2.61ddan  814  pm2.61dda  815  pm2.61da2ne  3021  ralimdvva  3185  reximdvva  3186  2ralbidva  3200  2rexbidva  3201  2ralbida  3261  spcimgft  3492  copsexgw  5438  copsexg  5439  pofun  5550  imainss  6112  fvmptdf  6948  eqfnfv2  6978  fnex  7165  f1elima  7211  fliftfun  7260  isores2  7281  f1oiso  7299  ovmpodxf  7510  sorpssuni  7679  sorpssint  7680  tfindsg2  7806  2ndconst  8044  poxp2  8086  sexp3  8096  poseq  8101  oalim  8460  omlim  8461  oaass  8489  omlimcl  8506  omass  8508  oelim2  8524  oeoa  8526  oeoelem  8527  nnaass  8551  omabs  8580  eroveu  8752  sbthlem4  9021  fimaxg  9190  fisupg  9191  fofinf1o  9235  fiming  9406  fiinfg  9407  ordtypelem7  9432  hartogs  9452  card2on  9462  unwdomg  9492  wemapwe  9609  frmin  9664  dfac5  10042  cfsmolem  10183  isf32lem2  10267  ttukeylem6  10427  ondomon  10476  alephreg  10496  ltexprlem6  10955  recexsrlem  11017  wloglei  11673  recextlem2  11772  fimaxre  12091  creur  12144  uz11  12804  xrmaxeq  13122  xrmineq  13123  xaddf  13167  xaddass  13192  xleadd1a  13196  xlt2add  13203  xmullem  13207  xmulgt0  13226  xmulasslem3  13229  xlemul1a  13231  xadddilem  13237  fzrevral  13557  seqcaopr2  13991  expnlbnd2  14187  faclbnd4lem4  14249  hashgt23el  14377  rtrclreclem3  15013  rtrclreclem4  15014  relexpindlem  15016  rtrclind  15018  shftlem  15021  01sqrex  15202  cau3lem  15308  limsupbnd2  15436  clim2  15457  clim2c  15458  clim0c  15460  rlimresb  15518  2clim  15525  climabs0  15538  climcn1  15545  climcn2  15546  o1rlimmul  15572  climsqz  15594  climsqz2  15595  rlimsqzlem  15602  lo1le  15605  climsup  15623  caucvgrlem2  15628  iseralt  15638  summolem2  15669  fsum2dlem  15723  cvgcmp  15770  cvgcmpce  15772  climfsum  15774  fsumiun  15775  geomulcvg  15832  mertenslem2  15841  mertens  15842  prodfn0  15850  prodfrec  15851  zprod  15893  fprodeq0  15931  fprodn0  15935  fprod2dlem  15936  smu01lem  16445  gcdcllem1  16459  dvdssq  16527  lcmdvds  16568  coprmdvds2  16614  pclem  16800  pcge0  16824  pcgcd1  16839  prmpwdvds  16866  1arithlem4  16888  4sqlem18  16924  vdwlem10  16952  vdwlem11  16953  ramval  16970  ramub1lem2  16989  ramcl  16991  imasaddfnlem  17483  imasaddflem  17485  imasvscafn  17492  imasleval  17496  ismon2  17692  isepi2  17699  issubc3  17807  cofucl  17846  setcmon  18045  setcepi  18046  ipodrsfi  18496  ipodrsima  18498  isacs3lem  18499  grpidpropd  18621  grprida  18634  gsumpropd2lem  18638  mgmhmpropd  18657  mgmhmima  18674  mhmpropd  18751  mhmimalem  18783  grplcan  18967  dfgrp3lem  19005  mulgdirlem  19072  subgmulg  19107  issubg4  19112  subgint  19117  ssnmz  19132  cycsubgcl  19172  gastacl  19275  orbsta  19279  cntzsubg  19305  galactghm  19370  odmulg  19522  odbezout  19524  sylow3lem2  19594  lsmsubm  19619  efgsfo  19705  mulgmhm  19793  mulgghm  19794  gsumval3  19873  gsumcllem  19874  gsumpt  19928  gsum2d  19938  gsum2d2  19940  prdsgsum  19947  subgdmdprd  20002  dprd2d2  20012  ablfac1eu  20041  rngpropd  20146  srglmhm  20193  srgrmhm  20194  ringpropd  20260  ringlghm  20284  pwsgprod  20300  dvdsrpropd  20387  rhmimasubrnglem  20533  cntzsdrg  20770  abvpropd  20803  islmodd  20852  lmodprop2d  20910  lsssubg  20943  lsspropd  21004  lmhmima  21034  lidlsubg  21213  phlpropd  21645  frlmsslsp  21786  lindfmm  21817  islindf4  21828  assapropd  21861  asclpropd  21887  psrass1lem  21922  mplcoe1  22025  mplcoe5  22028  mplind  22058  evlslem2  22067  evlsval  22074  coe1tmmul2  22251  mamuass  22377  mavmulass  22524  mdetuni0  22596  mdetmul  22598  cpmatacl  22691  cpmadugsumfi  22852  cpmadumatpolylem1  22856  cpmadumatpolylem2  22857  cpmadumatpoly  22858  cayhamlem4  22863  neips  23088  neindisj  23092  ordtrest2lem  23178  lmbrf  23235  lmss  23273  isreg2  23352  lmmo  23355  hauscmplem  23381  bwth  23385  2ndcomap  23433  1stcelcls  23436  restlly  23458  islly2  23459  cldllycmp  23470  comppfsc  23507  1stckgenlem  23528  txbas  23542  txbasval  23581  tx1cn  23584  ptpjopn  23587  ptcnp  23597  txnlly  23612  txlm  23623  xkococn  23635  fgabs  23854  fmfnfmlem4  23932  flimcf  23957  hauspwpwf1  23962  fclsbas  23996  fclscf  24000  flimfnfcls  24003  ghmcnp  24090  tsmsxp  24130  isxmet2d  24302  elmopn2  24420  mopni3  24469  blsscls2  24479  metequiv2  24485  metss2lem  24486  met2ndci  24497  metrest  24499  metcnp  24516  metcnp2  24517  metcnpi3  24521  txmetcnp  24522  nmolb2d  24693  xrge0tsms  24810  metdsre  24829  metnrmlem3  24837  fsumcn  24847  elcncf2  24867  mulc1cncf  24882  cncfco  24884  cncfmet  24886  bndth  24935  evth  24936  copco  24995  pcopt2  25000  pcoass  25001  pcorevlem  25003  lmmcvg  25238  lmmbrf  25239  iscau4  25256  iscauf  25257  cmetcaulem  25265  iscmet3lem3  25267  iscmet3lem1  25268  causs  25275  equivcfil  25276  lmclim  25280  caubl  25285  caublcls  25286  bcth3  25308  ivthle  25433  ivthle2  25434  ovoliunlem1  25479  ovolicc2lem5  25498  volsuplem  25532  uniioombllem6  25565  dyaddisjlem  25572  dyadmax  25575  volcn  25583  mbfmulc2lem  25624  ismbf3d  25631  mbfsup  25641  mbfinf  25642  mbflim  25645  i1fmullem  25671  itg2seq  25719  itg2uba  25720  itg2splitlem  25725  itg2split  25726  itg2monolem1  25727  bddiblnc  25819  ditgsplitlem  25837  ellimc2  25854  ellimc3  25856  limcflf  25858  limcmpt  25860  limcco  25870  lhop1lem  25990  dvfsumle  25998  dvfsumabs  26000  dvfsumrlim  26008  ftc1a  26014  ftc1lem6  26018  mdegmullem  26053  elply2  26171  plypf1  26187  ulmcaulem  26372  ulmcau  26373  ulmss  26375  ulmdvlem3  26380  mtest  26382  itgulm  26386  abelthlem8  26417  abelth  26419  tanord  26515  cxpcn3lem  26724  mcubic  26824  cubic2  26825  dvdsflsumcom  27165  fsumdvdsmul  27172  lgsdchrval  27331  2sqlem9  27404  rplogsumlem2  27462  rpvmasumlem  27464  dchrvmasumlem1  27472  vmalogdivsum2  27515  logsqvma  27519  selberg  27525  selberg4  27538  pntibndlem3  27569  pntlem3  27586  pntleml  27588  padicabv  27607  padicabvf  27608  padicabvcxp  27609  ostth3  27615  nosupbnd1lem5  27690  noinfbnd1lem5  27705  nocvxminlem  27760  lrrecfr  27949  addsprop  27982  mulsproplem9  28130  mulsproplem12  28133  mulsproplem13  28134  mulsproplem14  28135  mulsprop  28136  lemulsd  28144  mulsuniflem  28155  mulsasslem3  28171  axpasch  29024  axcontlem7  29053  axcontlem10  29056  cusgrsize2inds  29537  grpolcan  30616  nvmul0or  30736  nmosetre  30850  blocnilem  30890  blocni  30891  h2hcau  31065  h2hlm  31066  shsel3  31401  chscllem2  31724  homulcl  31845  adjsym  31919  cnvadj  31978  hhcno  31990  hhcnf  31991  lnopl  32000  unoplin  32006  counop  32007  lnfnl  32017  hmoplin  32028  hmopm  32107  nmcexi  32112  lnconi  32119  riesz3i  32148  leopmuli  32219  leopmul  32220  hstle  32316  mdsl0  32396  mdslmd1lem2  32412  atcvatlem  32471  chirredi  32480  cdj1i  32519  sbc2iedf  32549  foresf1o  32589  suppovss  32769  isoun  32790  difioo  32870  swrdf1  33031  xrge0tsmsd  33149  cycpmrn  33219  ressply1invg  33644  ply1unit  33650  fedgmullem2  33790  pstmxmet  34057  ordtrest2NEWlem  34082  esum2dlem  34252  esum2d  34253  dya2icoseg2  34438  eulerpartlemgc  34522  eulerpartlemgh  34538  eulerpartlemgs2  34540  ballotlemimin  34666  signstfvneq0  34732  hgt750lemb  34816  connpconn  35433  cvmliftmolem2  35480  cvmliftlem6  35488  cvmliftlem8  35490  cvmlift2lem12  35512  elmrsubrn  35718  dfon2lem6  35984  ifscgr  36242  brsegle  36306  neibastop2lem  36558  bj-elabd2ALT  37248  bj-ismooredr2  37438  curf  37933  finixpnum  37940  fin2solem  37941  fin2so  37942  lindsenlbs  37950  matunitlindflem1  37951  matunitlindflem2  37952  matunitlindf  37953  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem14  37969  poimirlem16  37971  poimirlem19  37974  poimirlem22  37977  poimirlem28  37983  poimirlem29  37984  poimirlem30  37985  poimir  37988  heicant  37990  itg2gt0cn  38010  ftc1cnnc  38027  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anc  38036  cover2  38050  filbcmb  38075  fdc  38080  fdc1  38081  seqpo  38082  incsequz  38083  incsequz2  38084  metf1o  38090  lmclim2  38093  geomcau  38094  isbnd2  38118  bndss  38121  ismtybndlem  38141  heibor1lem  38144  rrncmslem  38167  rrnequiv  38170  exidreslem  38212  ghomco  38226  isdrngo3  38294  rngoisocnv  38316  isidlc  38350  idlnegcl  38357  divrngidl  38363  intidl  38364  unichnidl  38366  keridl  38367  igenmin  38399  prnc  38402  ispridlc  38405  erimeq2  39098  prter3  39342  glbconxN  39838  atltcvr  39895  3dim1  39927  lvolnle3at  40042  linepsubN  40212  osumclN  40427  pexmidALTN  40438  lhpmatb  40491  cdlemg1idlemN  41032  dihlss  41710  dihglblem5aN  41752  dihatlat  41794  aks6d1c1p1  42560  aks6d1c5lem1  42589  unitscyglem4  42651  f1o2d2  42688  selvvvval  43032  fsuppind  43037  fsuppssindlem1  43038  prjspertr  43052  prjspreln0  43056  lsmfgcl  43520  kercvrlsm  43529  unxpwdom3  43541  hbt  43576  oa0suclim  43721  om0suclim  43722  oe0suclim  43723  naddcnff  43808  cvgdvgrat  44758  climinf  46054  clim2f  46082  clim2cf  46096  clim0cf  46100  clim2f2  46116  fmtnofac2lem  48043  ovmpordxf  48827  oppcthinendcALT  49928  cotsqcscsq  50249  aacllem  50288