Theorem anassrs 380

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  anass  381  mpanr1  413  anass1rs  505  anabss5  512  anabss7  517  2ralbida  2345  2rexbidva  2347  pofun  4049  issod  4056  imainss  4739  fvelimab  5229  eqfnfv2  5266  funconstss  5285  fnex  5383  rexima  5394  ralima  5395  f1elima  5412  fliftfun  5436  isores2  5453  isosolem  5463  f1oiso  5465  ovmpt2dxf  5626  grpridd  5697  tfrlemibxssdm  5941  oav2  6043  omv2  6045  nnaass  6064  eroveu  6197  prarloclem4  6596  genpml  6615  genpmu  6616  genpassl  6622  genpassu  6623  prmuloc2  6665  addcomprg  6676  mulcomprg  6678  ltaddpr  6695  ltexprlemloc  6705  addcanprlemu  6713  recexgt0sr  6858  reapmul1  7586  apreim  7594  recexaplem2  7633  creur  7911  uz11  8495  fzrevral  8967  iseqcaopr2  9241  expnlbnd2  9374  shftlem  9417  resqrexlemgt0  9618  cau3lem  9710  clim2  9804  clim2c  9805  clim0c  9807  2clim  9822  climabs0  9828  climcn1  9829  climcn2  9830  climsqz  9855  climsqz2  9856