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  655  anabss5  668  anabss7  673  mpanr1  703  pm2.61ddan  813  pm2.61dda  814  pm2.61da2ne  3013  ralimdvva  3184  reximdvva  3185  2ralbidva  3199  2rexbidva  3200  2ralbida  3260  spcimgft  3512  copsexgw  5450  copsexg  5451  pofun  5564  imainss  6127  fvmptdf  6974  eqfnfv2  7004  fnex  7191  f1elima  7238  fliftfun  7287  isores2  7308  f1oiso  7326  ovmpodxf  7539  sorpssuni  7708  sorpssint  7709  tfindsg2  7838  2ndconst  8080  poxp2  8122  sexp3  8132  poseq  8137  oalim  8496  omlim  8497  oaass  8525  omlimcl  8542  omass  8544  oelim2  8559  oeoa  8561  oeoelem  8562  nnaass  8586  omabs  8615  eroveu  8785  sbthlem4  9054  fimaxg  9234  fisupg  9235  fofinf1o  9283  fiming  9451  fiinfg  9452  ordtypelem7  9477  hartogs  9497  card2on  9507  unwdomg  9537  wemapwe  9650  frmin  9702  dfac5  10082  cfsmolem  10223  isf32lem2  10307  ttukeylem6  10467  ondomon  10516  alephreg  10535  ltexprlem6  10994  recexsrlem  11056  wloglei  11710  recextlem2  11809  fimaxre  12127  creur  12180  uz11  12818  xrmaxeq  13139  xrmineq  13140  xaddf  13184  xaddass  13209  xleadd1a  13213  xlt2add  13220  xmullem  13224  xmulgt0  13243  xmulasslem3  13246  xlemul1a  13248  xadddilem  13254  fzrevral  13573  seqcaopr2  14003  expnlbnd2  14199  faclbnd4lem4  14261  hashgt23el  14389  rtrclreclem3  15026  rtrclreclem4  15027  relexpindlem  15029  rtrclind  15031  shftlem  15034  01sqrex  15215  cau3lem  15321  limsupbnd2  15449  clim2  15470  clim2c  15471  clim0c  15473  rlimresb  15531  2clim  15538  climabs0  15551  climcn1  15558  climcn2  15559  o1rlimmul  15585  climsqz  15607  climsqz2  15608  rlimsqzlem  15615  lo1le  15618  climsup  15636  caucvgrlem2  15641  iseralt  15651  summolem2  15682  fsum2dlem  15736  cvgcmp  15782  cvgcmpce  15784  climfsum  15786  fsumiun  15787  geomulcvg  15842  mertenslem2  15851  mertens  15852  prodfn0  15860  prodfrec  15861  zprod  15903  fprodeq0  15941  fprodn0  15945  fprod2dlem  15946  smu01lem  16455  gcdcllem1  16469  dvdssq  16537  lcmdvds  16578  coprmdvds2  16624  pclem  16809  pcge0  16833  pcgcd1  16848  prmpwdvds  16875  1arithlem4  16897  4sqlem18  16933  vdwlem10  16961  vdwlem11  16962  ramval  16979  ramub1lem2  16998  ramcl  17000  imasaddfnlem  17491  imasaddflem  17493  imasvscafn  17500  imasleval  17504  ismon2  17696  isepi2  17703  issubc3  17811  cofucl  17850  setcmon  18049  setcepi  18050  ipodrsfi  18498  ipodrsima  18500  isacs3lem  18501  grpidpropd  18589  grprida  18602  gsumpropd2lem  18606  mgmhmpropd  18625  mgmhmima  18642  mhmpropd  18719  mhmimalem  18751  grplcan  18932  dfgrp3lem  18970  mulgdirlem  19037  subgmulg  19072  issubg4  19077  subgint  19082  ssnmz  19098  cycsubgcl  19138  gastacl  19241  orbsta  19245  cntzsubg  19271  galactghm  19334  odmulg  19486  odbezout  19488  sylow3lem2  19558  lsmsubm  19583  efgsfo  19669  mulgmhm  19757  mulgghm  19758  gsumval3  19837  gsumcllem  19838  gsumpt  19892  gsum2d  19902  gsum2d2  19904  prdsgsum  19911  subgdmdprd  19966  dprd2d2  19976  ablfac1eu  20005  rngpropd  20083  srglmhm  20130  srgrmhm  20131  ringpropd  20197  ringlghm  20221  dvdsrpropd  20325  rhmimasubrnglem  20474  cntzsdrg  20711  abvpropd  20744  islmodd  20772  lmodprop2d  20830  lsssubg  20863  lsspropd  20924  lmhmima  20954  lidlsubg  21133  phlpropd  21564  frlmsslsp  21705  lindfmm  21736  islindf4  21747  assapropd  21781  asclpropd  21806  psrass1lem  21841  mplcoe1  21944  mplcoe5  21947  mplind  21977  evlslem2  21986  evlsval  21993  coe1tmmul2  22162  mamuass  22289  mavmulass  22436  mdetuni0  22508  mdetmul  22510  cpmatacl  22603  cpmadugsumfi  22764  cpmadumatpolylem1  22768  cpmadumatpolylem2  22769  cpmadumatpoly  22770  cayhamlem4  22775  neips  23000  neindisj  23004  ordtrest2lem  23090  lmbrf  23147  lmss  23185  isreg2  23264  lmmo  23267  hauscmplem  23293  bwth  23297  2ndcomap  23345  1stcelcls  23348  restlly  23370  islly2  23371  cldllycmp  23382  comppfsc  23419  1stckgenlem  23440  txbas  23454  txbasval  23493  tx1cn  23496  ptpjopn  23499  ptcnp  23509  txnlly  23524  txlm  23535  xkococn  23547  fgabs  23766  fmfnfmlem4  23844  flimcf  23869  hauspwpwf1  23874  fclsbas  23908  fclscf  23912  flimfnfcls  23915  ghmcnp  24002  tsmsxp  24042  isxmet2d  24215  elmopn2  24333  mopni3  24382  blsscls2  24392  metequiv2  24398  metss2lem  24399  met2ndci  24410  metrest  24412  metcnp  24429  metcnp2  24430  metcnpi3  24434  txmetcnp  24435  nmolb2d  24606  xrge0tsms  24723  metdsre  24742  metnrmlem3  24750  fsumcn  24761  elcncf2  24783  mulc1cncf  24798  cncfco  24800  cncfmet  24802  bndth  24857  evth  24858  copco  24918  pcopt2  24923  pcoass  24924  pcorevlem  24926  lmmcvg  25161  lmmbrf  25162  iscau4  25179  iscauf  25180  cmetcaulem  25188  iscmet3lem3  25190  iscmet3lem1  25191  causs  25198  equivcfil  25199  lmclim  25203  caubl  25208  caublcls  25209  bcth3  25231  ivthle  25357  ivthle2  25358  ovoliunlem1  25403  ovolicc2lem5  25422  volsuplem  25456  uniioombllem6  25489  dyaddisjlem  25496  dyadmax  25499  volcn  25507  mbfmulc2lem  25548  ismbf3d  25555  mbfsup  25565  mbfinf  25566  mbflim  25569  i1fmullem  25595  itg2seq  25643  itg2uba  25644  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  bddiblnc  25743  ditgsplitlem  25761  ellimc2  25778  ellimc3  25780  limcflf  25782  limcmpt  25784  limcco  25794  lhop1lem  25918  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumrlim  25938  ftc1a  25944  ftc1lem6  25948  mdegmullem  25983  elply2  26101  plypf1  26117  ulmcaulem  26303  ulmcau  26304  ulmss  26306  ulmdvlem3  26311  mtest  26313  itgulm  26317  abelthlem8  26349  abelth  26351  tanord  26447  cxpcn3lem  26657  mcubic  26757  cubic2  26758  dvdsflsumcom  27098  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  lgsdchrval  27265  2sqlem9  27338  rplogsumlem2  27396  rpvmasumlem  27398  dchrvmasumlem1  27406  vmalogdivsum2  27449  logsqvma  27453  selberg  27459  selberg4  27472  pntibndlem3  27503  pntlem3  27520  pntleml  27522  padicabv  27541  padicabvf  27542  padicabvcxp  27543  ostth3  27549  nosupbnd1lem5  27624  noinfbnd1lem5  27639  nocvxminlem  27689  lrrecfr  27850  addsprop  27883  mulsproplem9  28027  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  mulsprop  28033  slemuld  28041  mulsuniflem  28052  mulsasslem3  28068  axpasch  28868  axcontlem7  28897  axcontlem10  28900  cusgrsize2inds  29381  grpolcan  30459  nvmul0or  30579  nmosetre  30693  blocnilem  30733  blocni  30734  h2hcau  30908  h2hlm  30909  shsel3  31244  chscllem2  31567  homulcl  31688  adjsym  31762  cnvadj  31821  hhcno  31833  hhcnf  31834  lnopl  31843  unoplin  31849  counop  31850  lnfnl  31860  hmoplin  31871  hmopm  31950  nmcexi  31955  lnconi  31962  riesz3i  31991  leopmuli  32062  leopmul  32063  hstle  32159  mdsl0  32239  mdslmd1lem2  32255  atcvatlem  32314  chirredi  32323  cdj1i  32362  sbc2iedf  32394  foresf1o  32433  suppovss  32604  isoun  32625  difioo  32705  swrdf1  32878  xrge0tsmsd  33002  cycpmrn  33100  ressply1invg  33538  ply1unit  33544  fedgmullem2  33626  pstmxmet  33887  ordtrest2NEWlem  33912  esum2dlem  34082  esum2d  34083  dya2icoseg2  34269  eulerpartlemgc  34353  eulerpartlemgh  34369  eulerpartlemgs2  34371  ballotlemimin  34497  signstfvneq0  34563  hgt750lemb  34647  connpconn  35222  cvmliftmolem2  35269  cvmliftlem6  35277  cvmliftlem8  35279  cvmlift2lem12  35301  elmrsubrn  35507  dfon2lem6  35776  ifscgr  36032  brsegle  36096  neibastop2lem  36348  bj-elabd2ALT  36913  bj-ismooredr2  37098  curf  37592  finixpnum  37599  fin2solem  37600  fin2so  37601  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem14  37628  poimirlem16  37630  poimirlem19  37633  poimirlem22  37636  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimir  37647  heicant  37649  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anc  37695  cover2  37709  filbcmb  37734  fdc  37739  fdc1  37740  seqpo  37741  incsequz  37742  incsequz2  37743  metf1o  37749  lmclim2  37752  geomcau  37753  isbnd2  37777  bndss  37780  ismtybndlem  37800  heibor1lem  37803  rrncmslem  37826  rrnequiv  37829  exidreslem  37871  ghomco  37885  isdrngo3  37953  rngoisocnv  37975  isidlc  38009  idlnegcl  38016  divrngidl  38022  intidl  38023  unichnidl  38025  keridl  38026  igenmin  38058  prnc  38061  ispridlc  38064  erimeq2  38670  prter3  38875  glbconxN  39372  atltcvr  39429  3dim1  39461  lvolnle3at  39576  linepsubN  39746  osumclN  39961  pexmidALTN  39972  lhpmatb  40025  cdlemg1idlemN  40566  dihlss  41244  dihglblem5aN  41286  dihatlat  41328  aks6d1c1p1  42095  aks6d1c5lem1  42124  unitscyglem4  42186  f1o2d2  42221  pwsgprod  42532  selvvvval  42573  fsuppind  42578  fsuppssindlem1  42579  prjspertr  42593  prjspreln0  42597  lsmfgcl  43063  kercvrlsm  43072  unxpwdom3  43084  hbt  43119  oa0suclim  43264  om0suclim  43265  oe0suclim  43266  naddcnff  43351  cvgdvgrat  44302  climinf  45604  clim2f  45634  clim2cf  45648  clim0cf  45652  clim2f2  45668  fmtnofac2lem  47569  ovmpordxf  48327  oppcthinendcALT  49430  cotsqcscsq  49751  aacllem  49790