Theorem anassrs 398

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  anass  399  mpanr1  434  anass1rs  561  anabss5  568  anabss7  573  2ralbida  2487  2rexbidva  2489  ralimdvva  2535  pofun  4290  issod  4297  imainss  5019  fvelimab  5542  eqfnfv2  5584  funconstss  5603  fnex  5707  rexima  5723  ralima  5724  f1elima  5741  fliftfun  5764  isores2  5781  isosolem  5792  f1oiso  5794  ovmpodxf  5967  tfrlemibxssdm  6295  oav2  6431  omv2  6433  nnaass  6453  eroveu  6592  prarloclem4  7439  genpml  7458  genpmu  7459  genpassl  7465  genpassu  7466  prmuloc2  7508  addcomprg  7519  mulcomprg  7521  ltaddpr  7538  ltexprlemloc  7548  addcanprlemu  7556  recexgt0sr  7714  reapmul1  8493  apreim  8501  recexaplem2  8549  creur  8854  uz11  9488  xaddass  9805  xleadd1a  9809  xlt2add  9816  fzrevral  10040  seq3caopr2  10417  expnlbnd2  10580  shftlem  10758  resqrexlemgt0  10962  cau3lem  11056  clim2  11224  clim2c  11225  clim0c  11227  2clim  11242  climabs0  11248  climcn1  11249  climcn2  11250  climsqz  11276  climsqz2  11277  summodclem2  11323  fsum2dlemstep  11375  fsumiun  11418  mertenslem2  11477  mertensabs  11478  prodfrecap  11487  fprodeq0  11558  fprod2dlemstep  11563  gcdmultiplez  11954  dvdssq  11964  lcmgcdlem  12009  lcmdvds  12011  coprmdvds2  12025  pclemub  12219  pcge0  12244  pcgcd1  12259  prmpwdvds  12285  1arithlem4  12296  grpidpropdg  12605  grpridd  12618  neipsm  12794  lmbrf  12855  lmss  12886  txbas  12898  txbasval  12907  tx1cn  12909  txlm  12919  isxmet2d  12988  elmopn2  13089  mopni3  13124  blsscls2  13133  metequiv2  13136  metss2lem  13137  metrest  13146  metcnp  13152  metcnp2  13153  metcnpi3  13157  elcncf2  13201  mulc1cncf  13216  cncfco  13218  cncfmet  13219  2sqlem9  13600