Theorem anassrs 466

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 419	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 416	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anass  467  anass1rs  651  anabss5  664  anabss7  669  mpanr1  699  pm2.61ddan  810  pm2.61dda  811  pm2.61da2ne  3028  ralimdvva  3202  reximdvva  3203  2ralbidva  3214  2rexbidva  3215  2ralbida  3278  copsexgw  5489  copsexg  5490  pofun  5605  imainss  6152  fvmptdf  7003  eqfnfv2  7032  fnex  7220  f1elima  7264  fliftfun  7311  isores2  7332  f1oiso  7350  ovmpodxf  7560  sorpssuni  7724  sorpssint  7725  tfindsg2  7853  2ndconst  8089  poxp2  8131  sexp3  8141  poseq  8146  oalim  8534  omlim  8535  oaass  8563  omlimcl  8580  omass  8582  oelim2  8597  oeoa  8599  oeoelem  8600  nnaass  8624  omabs  8652  eroveu  8808  sbthlem4  9088  fimaxg  9292  fisupg  9293  fofinf1o  9329  fiming  9495  fiinfg  9496  ordtypelem7  9521  hartogs  9541  card2on  9551  unwdomg  9581  wemapwe  9694  frmin  9746  dfac5  10125  cfsmolem  10267  isf32lem2  10351  ttukeylem6  10511  ondomon  10560  alephreg  10579  ltexprlem6  11038  recexsrlem  11100  wloglei  11750  recextlem2  11849  fimaxre  12162  creur  12210  uz11  12851  xrmaxeq  13162  xrmineq  13163  xaddf  13207  xaddass  13232  xleadd1a  13236  xlt2add  13243  xmullem  13247  xmulgt0  13266  xmulasslem3  13269  xlemul1a  13271  xadddilem  13277  fzrevral  13590  seqcaopr2  14008  expnlbnd2  14201  faclbnd4lem4  14260  hashgt23el  14388  rtrclreclem3  15011  rtrclreclem4  15012  relexpindlem  15014  rtrclind  15016  shftlem  15019  01sqrex  15200  cau3lem  15305  limsupbnd2  15431  clim2  15452  clim2c  15453  clim0c  15455  rlimresb  15513  2clim  15520  climabs0  15533  climcn1  15540  climcn2  15541  o1rlimmul  15567  climsqz  15589  climsqz2  15590  rlimsqzlem  15599  lo1le  15602  climsup  15620  caucvgrlem2  15625  iseralt  15635  summolem2  15666  fsum2dlem  15720  cvgcmp  15766  cvgcmpce  15768  climfsum  15770  fsumiun  15771  geomulcvg  15826  mertenslem2  15835  mertens  15836  prodfn0  15844  prodfrec  15845  zprod  15885  fprodeq0  15923  fprodn0  15927  fprod2dlem  15928  smu01lem  16430  gcdcllem1  16444  dvdssq  16508  lcmdvds  16549  coprmdvds2  16595  pclem  16775  pcge0  16799  pcgcd1  16814  prmpwdvds  16841  1arithlem4  16863  4sqlem18  16899  vdwlem10  16927  vdwlem11  16928  ramval  16945  ramub1lem2  16964  ramcl  16966  imasaddfnlem  17478  imasaddflem  17480  imasvscafn  17487  imasleval  17491  ismon2  17685  isepi2  17692  issubc3  17803  cofucl  17842  setcmon  18041  setcepi  18042  ipodrsfi  18496  ipodrsima  18498  isacs3lem  18499  grpidpropd  18587  grprida  18600  gsumpropd2lem  18604  mgmhmpropd  18623  mgmhmima  18640  mhmpropd  18714  mhmimalem  18741  grplcan  18921  dfgrp3lem  18957  mulgdirlem  19021  subgmulg  19056  issubg4  19061  subgint  19066  ssnmz  19082  cycsubgcl  19121  gastacl  19214  orbsta  19218  cntzsubg  19244  galactghm  19313  odmulg  19465  odbezout  19467  sylow3lem2  19537  lsmsubm  19562  efgsfo  19648  mulgmhm  19736  mulgghm  19737  gsumval3  19816  gsumcllem  19817  gsumpt  19871  gsum2d  19881  gsum2d2  19883  prdsgsum  19890  subgdmdprd  19945  dprd2d2  19955  ablfac1eu  19984  rngpropd  20068  srglmhm  20115  srgrmhm  20116  ringpropd  20176  ringlghm  20200  dvdsrpropd  20307  rhmimasubrnglem  20453  cntzsdrg  20561  abvpropd  20593  islmodd  20620  lmodprop2d  20678  lsssubg  20712  lsspropd  20772  lmhmima  20802  lidlsubg  20987  phlpropd  21427  frlmsslsp  21570  lindfmm  21601  islindf4  21612  assapropd  21645  asclpropd  21670  psrass1lemOLD  21712  psrass1lem  21715  mplcoe1  21811  mplcoe5  21814  mplind  21850  evlslem2  21861  evlsval  21868  coe1tmmul2  22018  mamuass  22122  mavmulass  22271  mdetuni0  22343  mdetmul  22345  cpmatacl  22438  cpmadugsumfi  22599  cpmadumatpolylem1  22603  cpmadumatpolylem2  22604  cpmadumatpoly  22605  cayhamlem4  22610  neips  22837  neindisj  22841  ordtrest2lem  22927  lmbrf  22984  lmss  23022  isreg2  23101  lmmo  23104  hauscmplem  23130  bwth  23134  2ndcomap  23182  1stcelcls  23185  restlly  23207  islly2  23208  cldllycmp  23219  comppfsc  23256  1stckgenlem  23277  txbas  23291  txbasval  23330  tx1cn  23333  ptpjopn  23336  ptcnp  23346  txnlly  23361  txlm  23372  xkococn  23384  fgabs  23603  fmfnfmlem4  23681  flimcf  23706  hauspwpwf1  23711  fclsbas  23745  fclscf  23749  flimfnfcls  23752  ghmcnp  23839  tsmsxp  23879  isxmet2d  24053  elmopn2  24171  mopni3  24223  blsscls2  24233  metequiv2  24239  metss2lem  24240  met2ndci  24251  metrest  24253  metcnp  24270  metcnp2  24271  metcnpi3  24275  txmetcnp  24276  nmolb2d  24455  xrge0tsms  24570  metdsre  24589  metnrmlem3  24597  fsumcn  24608  elcncf2  24630  mulc1cncf  24645  cncfco  24647  cncfmet  24649  bndth  24704  evth  24705  copco  24765  pcopt2  24770  pcoass  24771  pcorevlem  24773  lmmcvg  25009  lmmbrf  25010  iscau4  25027  iscauf  25028  cmetcaulem  25036  iscmet3lem3  25038  iscmet3lem1  25039  causs  25046  equivcfil  25047  lmclim  25051  caubl  25056  caublcls  25057  bcth3  25079  ivthle  25205  ivthle2  25206  ovoliunlem1  25251  ovolicc2lem5  25270  volsuplem  25304  uniioombllem6  25337  dyaddisjlem  25344  dyadmax  25347  volcn  25355  mbfmulc2lem  25396  ismbf3d  25403  mbfsup  25413  mbfinf  25414  mbflim  25417  i1fmullem  25443  itg2seq  25492  itg2uba  25493  itg2splitlem  25498  itg2split  25499  itg2monolem1  25500  bddiblnc  25591  ditgsplitlem  25609  ellimc2  25626  ellimc3  25628  limcflf  25630  limcmpt  25632  limcco  25642  lhop1lem  25765  dvfsumle  25773  dvfsumabs  25775  dvfsumrlim  25783  ftc1a  25789  ftc1lem6  25793  mdegmullem  25831  elply2  25945  plypf1  25961  ulmcaulem  26142  ulmcau  26143  ulmss  26145  ulmdvlem3  26150  mtest  26152  itgulm  26156  abelthlem8  26187  abelth  26189  tanord  26283  cxpcn3lem  26491  mcubic  26588  cubic2  26589  dvdsflsumcom  26928  fsumdvdsmul  26935  lgsdchrval  27093  2sqlem9  27166  rplogsumlem2  27224  rpvmasumlem  27226  dchrvmasumlem1  27234  vmalogdivsum2  27277  logsqvma  27281  selberg  27287  selberg4  27300  pntibndlem3  27331  pntlem3  27348  pntleml  27350  padicabv  27369  padicabvf  27370  padicabvcxp  27371  ostth3  27377  nosupbnd1lem5  27451  noinfbnd1lem5  27466  nocvxminlem  27515  lrrecfr  27665  addsprop  27698  mulsproplem9  27819  mulsproplem12  27822  mulsproplem13  27823  mulsproplem14  27824  mulsprop  27825  slemuld  27833  mulsuniflem  27843  mulsasslem3  27859  axpasch  28466  axcontlem7  28495  axcontlem10  28498  cusgrsize2inds  28977  grpolcan  30050  nvmul0or  30170  nmosetre  30284  blocnilem  30324  blocni  30325  h2hcau  30499  h2hlm  30500  shsel3  30835  chscllem2  31158  homulcl  31279  adjsym  31353  cnvadj  31412  hhcno  31424  hhcnf  31425  lnopl  31434  unoplin  31440  counop  31441  lnfnl  31451  hmoplin  31462  hmopm  31541  nmcexi  31546  lnconi  31553  riesz3i  31582  leopmuli  31653  leopmul  31654  hstle  31750  mdsl0  31830  mdslmd1lem2  31846  atcvatlem  31905  chirredi  31914  cdj1i  31953  sbc2iedf  31974  foresf1o  32009  suppovss  32173  isoun  32190  difioo  32260  swrdf1  32387  xrge0tsmsd  32479  cycpmrn  32572  ressply1invg  32932  fedgmullem2  33003  pstmxmet  33175  ordtrest2NEWlem  33200  esum2dlem  33388  esum2d  33389  dya2icoseg2  33575  eulerpartlemgc  33659  eulerpartlemgh  33675  eulerpartlemgs2  33677  ballotlemimin  33802  signstfvneq0  33881  hgt750lemb  33966  connpconn  34524  cvmliftmolem2  34571  cvmliftlem6  34579  cvmliftlem8  34581  cvmlift2lem12  34603  elmrsubrn  34809  dfon2lem6  35064  ifscgr  35320  brsegle  35384  gg-dvfsumle  35468  neibastop2lem  35548  bj-elabd2ALT  36108  bj-ismooredr2  36294  curf  36769  finixpnum  36776  fin2solem  36777  fin2so  36778  lindsenlbs  36786  matunitlindflem1  36787  matunitlindflem2  36788  matunitlindf  36789  poimirlem3  36794  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem14  36805  poimirlem16  36807  poimirlem19  36810  poimirlem22  36813  poimirlem28  36819  poimirlem29  36820  poimirlem30  36821  poimir  36824  heicant  36826  itg2gt0cn  36846  ftc1cnnc  36863  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anc  36872  cover2  36886  filbcmb  36911  fdc  36916  fdc1  36917  seqpo  36918  incsequz  36919  incsequz2  36920  metf1o  36926  lmclim2  36929  geomcau  36930  isbnd2  36954  bndss  36957  ismtybndlem  36977  heibor1lem  36980  rrncmslem  37003  rrnequiv  37006  exidreslem  37048  ghomco  37062  isdrngo3  37130  rngoisocnv  37152  isidlc  37186  idlnegcl  37193  divrngidl  37199  intidl  37200  unichnidl  37202  keridl  37203  igenmin  37235  prnc  37238  ispridlc  37241  erimeq2  37851  prter3  38055  glbconxN  38552  atltcvr  38609  3dim1  38641  lvolnle3at  38756  linepsubN  38926  osumclN  39141  pexmidALTN  39152  lhpmatb  39205  cdlemg1idlemN  39746  dihlss  40424  dihglblem5aN  40466  dihatlat  40508  metakunt1  41291  metakunt2  41292  f1o2d2  41361  pwsgprod  41416  selvvvval  41459  fsuppind  41464  fsuppssindlem1  41465  prjspertr  41649  prjspreln0  41653  lsmfgcl  42118  kercvrlsm  42127  unxpwdom3  42139  hbt  42174  oa0suclim  42327  om0suclim  42328  oe0suclim  42329  naddcnff  42414  cvgdvgrat  43374  climinf  44620  clim2f  44650  clim2cf  44664  clim0cf  44668  clim2f2  44684  fmtnofac2lem  46534  isomuspgrlem2d  46797  ovmpordxf  47102  cotsqcscsq  47894  aacllem  47935