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

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

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

This theorem is referenced by:  anass  469  anass1rs  653  anabss5  666  anabss7  671  mpanr1  701  pm2.61ddan  812  pm2.61dda  813  pm2.61da2ne  3029  ralimdvva  3197  reximdvva  3198  2ralbidva  3206  2rexbidva  3207  2ralbida  3264  copsexgw  5452  copsexg  5453  pofun  5568  imainss  6111  fvmptdf  6959  eqfnfv2  6988  fnex  7172  f1elima  7215  fliftfun  7262  isores2  7283  f1oiso  7301  ovmpodxf  7510  sorpssuni  7674  sorpssint  7675  tfindsg2  7803  2ndconst  8038  poxp2  8080  sexp3  8090  poseq  8095  oalim  8483  omlim  8484  oaass  8513  omlimcl  8530  omass  8532  oelim2  8547  oeoa  8549  oeoelem  8550  nnaass  8574  omabs  8602  eroveu  8758  sbthlem4  9037  fimaxg  9241  fisupg  9242  fofinf1o  9278  fiming  9443  fiinfg  9444  ordtypelem7  9469  hartogs  9489  card2on  9499  unwdomg  9529  wemapwe  9642  frmin  9694  dfac5  10073  cfsmolem  10215  isf32lem2  10299  ttukeylem6  10459  ondomon  10508  alephreg  10527  ltexprlem6  10986  recexsrlem  11048  wloglei  11696  recextlem2  11795  fimaxre  12108  creur  12156  uz11  12797  xrmaxeq  13108  xrmineq  13109  xaddf  13153  xaddass  13178  xleadd1a  13182  xlt2add  13189  xmullem  13193  xmulgt0  13212  xmulasslem3  13215  xlemul1a  13217  xadddilem  13223  fzrevral  13536  seqcaopr2  13954  expnlbnd2  14147  faclbnd4lem4  14206  hashgt23el  14334  rtrclreclem3  14957  rtrclreclem4  14958  relexpindlem  14960  rtrclind  14962  shftlem  14965  01sqrex  15146  cau3lem  15251  limsupbnd2  15377  clim2  15398  clim2c  15399  clim0c  15401  rlimresb  15459  2clim  15466  climabs0  15479  climcn1  15486  climcn2  15487  o1rlimmul  15513  climsqz  15535  climsqz2  15536  rlimsqzlem  15545  lo1le  15548  climsup  15566  caucvgrlem2  15571  iseralt  15581  summolem2  15612  fsum2dlem  15666  cvgcmp  15712  cvgcmpce  15714  climfsum  15716  fsumiun  15717  geomulcvg  15772  mertenslem2  15781  mertens  15782  prodfn0  15790  prodfrec  15791  zprod  15831  fprodeq0  15869  fprodn0  15873  fprod2dlem  15874  smu01lem  16376  gcdcllem1  16390  dvdssq  16454  lcmdvds  16495  coprmdvds2  16541  pclem  16721  pcge0  16745  pcgcd1  16760  prmpwdvds  16787  1arithlem4  16809  4sqlem18  16845  vdwlem10  16873  vdwlem11  16874  ramval  16891  ramub1lem2  16910  ramcl  16912  imasaddfnlem  17424  imasaddflem  17426  imasvscafn  17433  imasleval  17437  ismon2  17631  isepi2  17638  issubc3  17749  cofucl  17788  setcmon  17987  setcepi  17988  ipodrsfi  18442  ipodrsima  18444  isacs3lem  18445  grpidpropd  18531  grpridd  18544  gsumpropd2lem  18548  mhmpropd  18622  mhmima  18649  grplcan  18823  dfgrp3lem  18859  mulgdirlem  18921  subgmulg  18956  issubg4  18961  subgint  18966  ssnmz  18982  cycsubgcl  19013  gastacl  19103  orbsta  19107  cntzsubg  19131  galactghm  19200  odmulg  19352  odbezout  19354  sylow3lem2  19424  lsmsubm  19449  efgsfo  19535  mulgmhm  19620  mulgghm  19621  gsumval3  19698  gsumcllem  19699  gsumpt  19753  gsum2d  19763  gsum2d2  19765  prdsgsum  19772  subgdmdprd  19827  dprd2d2  19837  ablfac1eu  19866  srglmhm  19966  srgrmhm  19967  ringpropd  20020  ringlghm  20042  dvdsrpropd  20141  cntzsdrg  20325  abvpropd  20357  islmodd  20384  lmodprop2d  20441  lsssubg  20475  lsspropd  20535  lmhmima  20565  lidlsubg  20744  phlpropd  21096  frlmsslsp  21239  lindfmm  21270  islindf4  21281  assapropd  21312  asclpropd  21337  psrass1lemOLD  21379  psrass1lem  21382  mplcoe1  21475  mplcoe5  21478  mplind  21515  evlslem2  21526  evlsval  21533  coe1tmmul2  21684  mamuass  21786  mavmulass  21935  mdetuni0  22007  mdetmul  22009  cpmatacl  22102  cpmadugsumfi  22263  cpmadumatpolylem1  22267  cpmadumatpolylem2  22268  cpmadumatpoly  22269  cayhamlem4  22274  neips  22501  neindisj  22505  ordtrest2lem  22591  lmbrf  22648  lmss  22686  isreg2  22765  lmmo  22768  hauscmplem  22794  bwth  22798  2ndcomap  22846  1stcelcls  22849  restlly  22871  islly2  22872  cldllycmp  22883  comppfsc  22920  1stckgenlem  22941  txbas  22955  txbasval  22994  tx1cn  22997  ptpjopn  23000  ptcnp  23010  txnlly  23025  txlm  23036  xkococn  23048  fgabs  23267  fmfnfmlem4  23345  flimcf  23370  hauspwpwf1  23375  fclsbas  23409  fclscf  23413  flimfnfcls  23416  ghmcnp  23503  tsmsxp  23543  isxmet2d  23717  elmopn2  23835  mopni3  23887  blsscls2  23897  metequiv2  23903  metss2lem  23904  met2ndci  23915  metrest  23917  metcnp  23934  metcnp2  23935  metcnpi3  23939  txmetcnp  23940  nmolb2d  24119  xrge0tsms  24234  metdsre  24253  metnrmlem3  24261  fsumcn  24270  elcncf2  24290  mulc1cncf  24305  cncfco  24307  cncfmet  24309  bndth  24358  evth  24359  copco  24418  pcopt2  24423  pcoass  24424  pcorevlem  24426  lmmcvg  24662  lmmbrf  24663  iscau4  24680  iscauf  24681  cmetcaulem  24689  iscmet3lem3  24691  iscmet3lem1  24692  causs  24699  equivcfil  24700  lmclim  24704  caubl  24709  caublcls  24710  bcth3  24732  ivthle  24857  ivthle2  24858  ovoliunlem1  24903  ovolicc2lem5  24922  volsuplem  24956  uniioombllem6  24989  dyaddisjlem  24996  dyadmax  24999  volcn  25007  mbfmulc2lem  25048  ismbf3d  25055  mbfsup  25065  mbfinf  25066  mbflim  25069  i1fmullem  25095  itg2seq  25144  itg2uba  25145  itg2splitlem  25150  itg2split  25151  itg2monolem1  25152  bddiblnc  25243  ditgsplitlem  25261  ellimc2  25278  ellimc3  25280  limcflf  25282  limcmpt  25284  limcco  25294  lhop1lem  25414  dvfsumle  25422  dvfsumabs  25424  dvfsumrlim  25432  ftc1a  25438  ftc1lem6  25442  mdegmullem  25480  elply2  25594  plypf1  25610  ulmcaulem  25790  ulmcau  25791  ulmss  25793  ulmdvlem3  25798  mtest  25800  itgulm  25804  abelthlem8  25835  abelth  25837  tanord  25931  cxpcn3lem  26137  mcubic  26234  cubic2  26235  dvdsflsumcom  26574  fsumdvdsmul  26581  lgsdchrval  26739  2sqlem9  26812  rplogsumlem2  26870  rpvmasumlem  26872  dchrvmasumlem1  26880  vmalogdivsum2  26923  logsqvma  26927  selberg  26933  selberg4  26946  pntibndlem3  26977  pntlem3  26994  pntleml  26996  padicabv  27015  padicabvf  27016  padicabvcxp  27017  ostth3  27023  nosupbnd1lem5  27097  noinfbnd1lem5  27112  nocvxminlem  27160  lrrecfr  27298  addsprop  27331  axpasch  27953  axcontlem7  27982  axcontlem10  27985  cusgrsize2inds  28464  grpolcan  29535  nvmul0or  29655  nmosetre  29769  blocnilem  29809  blocni  29810  h2hcau  29984  h2hlm  29985  shsel3  30320  chscllem2  30643  homulcl  30764  adjsym  30838  cnvadj  30897  hhcno  30909  hhcnf  30910  lnopl  30919  unoplin  30925  counop  30926  lnfnl  30936  hmoplin  30947  hmopm  31026  nmcexi  31031  lnconi  31038  riesz3i  31067  leopmuli  31138  leopmul  31139  hstle  31235  mdsl0  31315  mdslmd1lem2  31331  atcvatlem  31390  chirredi  31399  cdj1i  31438  sbc2iedf  31459  foresf1o  31495  suppovss  31665  isoun  31683  difioo  31753  swrdf1  31880  xrge0tsmsd  31969  cycpmrn  32062  ressply1invg  32357  fedgmullem2  32412  pstmxmet  32567  ordtrest2NEWlem  32592  esum2dlem  32780  esum2d  32781  dya2icoseg2  32967  eulerpartlemgc  33051  eulerpartlemgh  33067  eulerpartlemgs2  33069  ballotlemimin  33194  signstfvneq0  33273  hgt750lemb  33358  connpconn  33916  cvmliftmolem2  33963  cvmliftlem6  33971  cvmliftlem8  33973  cvmlift2lem12  33995  elmrsubrn  34201  dfon2lem6  34449  ifscgr  34705  brsegle  34769  neibastop2lem  34908  bj-elabd2ALT  35468  bj-ismooredr2  35654  curf  36129  finixpnum  36136  fin2solem  36137  fin2so  36138  lindsenlbs  36146  matunitlindflem1  36147  matunitlindflem2  36148  matunitlindf  36149  poimirlem3  36154  poimirlem4  36155  poimirlem6  36157  poimirlem7  36158  poimirlem14  36165  poimirlem16  36167  poimirlem19  36170  poimirlem22  36173  poimirlem28  36179  poimirlem29  36180  poimirlem30  36181  poimir  36184  heicant  36186  itg2gt0cn  36206  ftc1cnnc  36223  ftc1anclem5  36228  ftc1anclem6  36229  ftc1anclem7  36230  ftc1anc  36232  cover2  36246  filbcmb  36272  fdc  36277  fdc1  36278  seqpo  36279  incsequz  36280  incsequz2  36281  metf1o  36287  lmclim2  36290  geomcau  36291  isbnd2  36315  bndss  36318  ismtybndlem  36338  heibor1lem  36341  rrncmslem  36364  rrnequiv  36367  exidreslem  36409  ghomco  36423  isdrngo3  36491  rngoisocnv  36513  isidlc  36547  idlnegcl  36554  divrngidl  36560  intidl  36561  unichnidl  36563  keridl  36564  igenmin  36596  prnc  36599  ispridlc  36602  erimeq2  37213  prter3  37417  glbconxN  37914  atltcvr  37971  3dim1  38003  lvolnle3at  38118  linepsubN  38288  osumclN  38503  pexmidALTN  38514  lhpmatb  38567  cdlemg1idlemN  39108  dihlss  39786  dihglblem5aN  39828  dihatlat  39870  metakunt1  40650  metakunt2  40651  pwsgprod  40790  fsuppind  40823  fsuppssindlem1  40824  prjspertr  41001  prjspreln0  41005  lsmfgcl  41459  kercvrlsm  41468  unxpwdom3  41480  hbt  41515  oa0suclim  41668  om0suclim  41669  oe0suclim  41670  naddcnff  41755  cvgdvgrat  42715  climinf  43967  clim2f  43997  clim2cf  44011  clim0cf  44015  clim2f2  44031  fmtnofac2lem  45880  isomuspgrlem2d  46143  mgmhmpropd  46199  mgmhmima  46216  ovmpordxf  46534  cotsqcscsq  47327  aacllem  47368