Theorem anassrs 404

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anass  405  mpanr1  441  anass1rs  577  anabss5  584  anabss7  589  2ralbida  2571  2rexbidva  2573  ralimdvva  2619  pofun  4455  issod  4462  imainss  5201  fvelimab  5756  eqfnfv2  5801  funconstss  5821  fnex  5931  rexima  5954  ralima  5955  f1elima  5973  fliftfun  5996  isores2  6013  isosolem  6024  f1oiso  6026  ovmpodxf  6208  tfrlemibxssdm  6592  oav2  6730  omv2  6732  nnaass  6752  eroveu  6894  prarloclem4  7859  genpml  7878  genpmu  7879  genpassl  7885  genpassu  7886  prmuloc2  7928  addcomprg  7939  mulcomprg  7941  ltaddpr  7958  ltexprlemloc  7968  addcanprlemu  7976  recexgt0sr  8134  reapmul1  8917  apreim  8925  recexaplem2  8974  creur  9283  uz11  9928  xaddass  10254  xleadd1a  10258  xlt2add  10265  fzrevral  10495  seq3caopr2  10913  seqcaopr2g  10914  expnlbnd2  11086  shftlem  11564  resqrexlemgt0  11769  cau3lem  11863  clim2  12032  clim2c  12033  clim0c  12035  2clim  12050  climabs0  12056  climcn1  12057  climcn2  12058  climsqz  12084  climsqz2  12085  summodclem2  12132  fsum2dlemstep  12184  fsumiun  12227  mertenslem2  12286  mertensabs  12287  prodfrecap  12296  fprodeq0  12367  fprod2dlemstep  12372  gcdmultiplez  12781  dvdssq  12791  lcmgcdlem  12838  lcmdvds  12840  coprmdvds2  12854  pclemub  13049  pcxqcl  13074  pcge0  13075  pcgcd1  13090  prmpwdvds  13117  1arithlem4  13128  4sqlem18  13170  imasaddfnlemg  13618  imasaddflemg  13620  grpidpropdg  13677  grprida  13690  mhmpropd  13756  mhmima  13781  grplcan  13850  dfgrp3mlem  13886  mulgdirlem  13939  subgmulg  13974  issubg4m  13979  subgintm  13984  ssnmz  13997  rngpropd  14237  srglmhm  14280  srgrmhm  14281  ringpropd  14326  ringlghm  14349  dvdsrpropdg  14437  isnzr2  14474  islmod  14610  islmodd  14612  lmodprop2d  14668  lsssubg  14697  lsspropdg  14751  lidlsubg  14806  expghmap  14925  assapropd  14997  asclpropd  15023  neipsm  15238  lmbrf  15299  lmss  15330  txbas  15342  txbasval  15351  tx1cn  15353  txlm  15363  isxmet2d  15432  elmopn2  15533  mopni3  15568  blsscls2  15577  metequiv2  15580  metss2lem  15581  metrest  15590  metcnp  15596  metcnp2  15597  metcnpi3  15601  elcncf2  15658  mulc1cncf  15673  cncfco  15675  cncfmet  15676  fsumdvdsmul  16088  2sqlem9  16226