Theorem anassrs 395

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  anass  396  mpanr1  431  anass1rs  543  anabss5  550  anabss7  555  2ralbida  2428  2rexbidva  2430  ralimdvva  2473  pofun  4192  issod  4199  imainss  4910  fvelimab  5429  eqfnfv2  5471  funconstss  5490  fnex  5594  rexima  5608  ralima  5609  f1elima  5626  fliftfun  5649  isores2  5666  isosolem  5677  f1oiso  5679  ovmpodxf  5848  grpridd  5919  tfrlemibxssdm  6176  oav2  6311  omv2  6313  nnaass  6333  eroveu  6472  prarloclem4  7248  genpml  7267  genpmu  7268  genpassl  7274  genpassu  7275  prmuloc2  7317  addcomprg  7328  mulcomprg  7330  ltaddpr  7347  ltexprlemloc  7357  addcanprlemu  7365  recexgt0sr  7510  reapmul1  8269  apreim  8277  recexaplem2  8320  creur  8621  uz11  9244  xaddass  9539  xleadd1a  9543  xlt2add  9550  fzrevral  9772  seq3caopr2  10142  expnlbnd2  10304  shftlem  10475  resqrexlemgt0  10678  cau3lem  10772  clim2  10938  clim2c  10939  clim0c  10941  2clim  10956  climabs0  10962  climcn1  10963  climcn2  10964  climsqz  10990  climsqz2  10991  summodclem2  11037  fsum2dlemstep  11089  fsumiun  11132  mertenslem2  11191  mertensabs  11192  gcdmultiplez  11549  dvdssq  11559  lcmgcdlem  11598  lcmdvds  11600  coprmdvds2  11614  neipsm  12160  lmbrf  12220  lmss  12251  txbas  12263  txbasval  12272  tx1cn  12274  txlm  12284  isxmet2d  12331  elmopn2  12432  mopni3  12467  blsscls2  12476  metequiv2  12479  metss2lem  12480  metrest  12489  metcnp  12495  metcnp2  12496  metcnpi3  12500  elcncf2  12541  mulc1cncf  12556  cncfco  12558  cncfmet  12559