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  2498  2rexbidva  2500  ralimdvva  2546  pofun  4314  issod  4321  imainss  5046  fvelimab  5575  eqfnfv2  5617  funconstss  5637  fnex  5741  rexima  5758  ralima  5759  f1elima  5777  fliftfun  5800  isores2  5817  isosolem  5828  f1oiso  5830  ovmpodxf  6003  tfrlemibxssdm  6331  oav2  6467  omv2  6469  nnaass  6489  eroveu  6629  prarloclem4  7500  genpml  7519  genpmu  7520  genpassl  7526  genpassu  7527  prmuloc2  7569  addcomprg  7580  mulcomprg  7582  ltaddpr  7599  ltexprlemloc  7609  addcanprlemu  7617  recexgt0sr  7775  reapmul1  8555  apreim  8563  recexaplem2  8612  creur  8919  uz11  9553  xaddass  9872  xleadd1a  9876  xlt2add  9883  fzrevral  10108  seq3caopr2  10485  expnlbnd2  10649  shftlem  10828  resqrexlemgt0  11032  cau3lem  11126  clim2  11294  clim2c  11295  clim0c  11297  2clim  11312  climabs0  11318  climcn1  11319  climcn2  11320  climsqz  11346  climsqz2  11347  summodclem2  11393  fsum2dlemstep  11445  fsumiun  11488  mertenslem2  11547  mertensabs  11548  prodfrecap  11557  fprodeq0  11628  fprod2dlemstep  11633  gcdmultiplez  12025  dvdssq  12035  lcmgcdlem  12080  lcmdvds  12082  coprmdvds2  12096  pclemub  12290  pcge0  12315  pcgcd1  12330  prmpwdvds  12356  1arithlem4  12367  imasaddfnlemg  12741  imasaddflemg  12743  grpidpropdg  12799  grpridd  12812  mhmpropd  12863  mhmima  12881  grplcan  12938  dfgrp3mlem  12974  mulgdirlem  13020  subgmulg  13054  issubg4m  13059  subgintm  13064  ssnmz  13077  srglmhm  13182  srgrmhm  13183  ringpropd  13223  dvdsrpropdg  13322  islmod  13387  islmodd  13389  lmodprop2d  13444  lsssubg  13470  lsspropdg  13523  lidlsubg  13571  neipsm  13794  lmbrf  13855  lmss  13886  txbas  13898  txbasval  13907  tx1cn  13909  txlm  13919  isxmet2d  13988  elmopn2  14089  mopni3  14124  blsscls2  14133  metequiv2  14136  metss2lem  14137  metrest  14146  metcnp  14152  metcnp2  14153  metcnpi3  14157  elcncf2  14201  mulc1cncf  14216  cncfco  14218  cncfmet  14219  2sqlem9  14611