Theorem anassrs 400

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  401  mpanr1  437  anass1rs  571  anabss5  578  anabss7  583  2ralbida  2511  2rexbidva  2513  ralimdvva  2559  pofun  4330  issod  4337  imainss  5062  fvelimab  5593  eqfnfv2  5635  funconstss  5655  fnex  5759  rexima  5776  ralima  5777  f1elima  5795  fliftfun  5818  isores2  5835  isosolem  5846  f1oiso  5848  ovmpodxf  6023  tfrlemibxssdm  6353  oav2  6489  omv2  6491  nnaass  6511  eroveu  6653  prarloclem4  7528  genpml  7547  genpmu  7548  genpassl  7554  genpassu  7555  prmuloc2  7597  addcomprg  7608  mulcomprg  7610  ltaddpr  7627  ltexprlemloc  7637  addcanprlemu  7645  recexgt0sr  7803  reapmul1  8583  apreim  8591  recexaplem2  8640  creur  8947  uz11  9582  xaddass  9901  xleadd1a  9905  xlt2add  9912  fzrevral  10137  seq3caopr2  10515  expnlbnd2  10680  shftlem  10860  resqrexlemgt0  11064  cau3lem  11158  clim2  11326  clim2c  11327  clim0c  11329  2clim  11344  climabs0  11350  climcn1  11351  climcn2  11352  climsqz  11378  climsqz2  11379  summodclem2  11425  fsum2dlemstep  11477  fsumiun  11520  mertenslem2  11579  mertensabs  11580  prodfrecap  11589  fprodeq0  11660  fprod2dlemstep  11665  gcdmultiplez  12057  dvdssq  12067  lcmgcdlem  12112  lcmdvds  12114  coprmdvds2  12128  pclemub  12322  pcxqcl  12347  pcge0  12348  pcgcd1  12363  prmpwdvds  12390  1arithlem4  12401  4sqlem18  12443  imasaddfnlemg  12794  imasaddflemg  12796  grpidpropdg  12853  grprida  12866  gsumpropd2  12871  mhmpropd  12933  mhmima  12958  grplcan  13021  dfgrp3mlem  13057  mulgdirlem  13110  subgmulg  13144  issubg4m  13149  subgintm  13154  ssnmz  13167  rngpropd  13326  srglmhm  13364  srgrmhm  13365  ringpropd  13409  dvdsrpropdg  13514  islmod  13624  islmodd  13626  lmodprop2d  13681  lsssubg  13710  lsspropdg  13764  lidlsubg  13819  neipsm  14131  lmbrf  14192  lmss  14223  txbas  14235  txbasval  14244  tx1cn  14246  txlm  14256  isxmet2d  14325  elmopn2  14426  mopni3  14461  blsscls2  14470  metequiv2  14473  metss2lem  14474  metrest  14483  metcnp  14489  metcnp2  14490  metcnpi3  14494  elcncf2  14538  mulc1cncf  14553  cncfco  14555  cncfmet  14556  2sqlem9  14949