Theorem anassrs 392

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  anass  393  mpanr1  427  anass1rs  535  anabss5  542  anabss7  547  2ralbida  2387  2rexbidva  2389  pofun  4067  issod  4074  imainss  4759  fvelimab  5250  eqfnfv2  5287  funconstss  5306  fnex  5404  rexima  5415  ralima  5416  f1elima  5433  fliftfun  5456  isores2  5473  isosolem  5483  f1oiso  5485  ovmpt2dxf  5646  grpridd  5717  tfrlemibxssdm  5964  oav2  6066  omv2  6068  nnaass  6087  eroveu  6220  prarloclem4  6688  genpml  6707  genpmu  6708  genpassl  6714  genpassu  6715  prmuloc2  6757  addcomprg  6768  mulcomprg  6770  ltaddpr  6787  ltexprlemloc  6797  addcanprlemu  6805  recexgt0sr  6950  reapmul1  7695  apreim  7703  recexaplem2  7742  creur  8036  uz11  8641  fzrevral  9122  iseqcaopr2  9461  expnlbnd2  9598  shftlem  9704  resqrexlemgt0  9906  cau3lem  10000  clim2  10122  clim2c  10123  clim0c  10125  2clim  10140  climabs0  10146  climcn1  10147  climcn2  10148  climsqz  10173  climsqz2  10174  gcdmultiplez  10410  dvdssq  10420  lcmgcdlem  10459  lcmdvds  10461  coprmdvds2  10475