Theorem anassrs 397

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 362	. 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  398  mpanr1  433  anass1rs  560  anabss5  567  anabss7  572  2ralbida  2454  2rexbidva  2456  ralimdvva  2499  pofun  4229  issod  4236  imainss  4949  fvelimab  5470  eqfnfv2  5512  funconstss  5531  fnex  5635  rexima  5649  ralima  5650  f1elima  5667  fliftfun  5690  isores2  5707  isosolem  5718  f1oiso  5720  ovmpodxf  5889  grpridd  5960  tfrlemibxssdm  6217  oav2  6352  omv2  6354  nnaass  6374  eroveu  6513  prarloclem4  7299  genpml  7318  genpmu  7319  genpassl  7325  genpassu  7326  prmuloc2  7368  addcomprg  7379  mulcomprg  7381  ltaddpr  7398  ltexprlemloc  7408  addcanprlemu  7416  recexgt0sr  7574  reapmul1  8350  apreim  8358  recexaplem2  8406  creur  8710  uz11  9341  xaddass  9645  xleadd1a  9649  xlt2add  9656  fzrevral  9878  seq3caopr2  10248  expnlbnd2  10410  shftlem  10581  resqrexlemgt0  10785  cau3lem  10879  clim2  11045  clim2c  11046  clim0c  11048  2clim  11063  climabs0  11069  climcn1  11070  climcn2  11071  climsqz  11097  climsqz2  11098  summodclem2  11144  fsum2dlemstep  11196  fsumiun  11239  mertenslem2  11298  mertensabs  11299  prodfrecap  11308  gcdmultiplez  11698  dvdssq  11708  lcmgcdlem  11747  lcmdvds  11749  coprmdvds2  11763  neipsm  12312  lmbrf  12373  lmss  12404  txbas  12416  txbasval  12425  tx1cn  12427  txlm  12437  isxmet2d  12506  elmopn2  12607  mopni3  12642  blsscls2  12651  metequiv2  12654  metss2lem  12655  metrest  12664  metcnp  12670  metcnp2  12671  metcnpi3  12675  elcncf2  12719  mulc1cncf  12734  cncfco  12736  cncfmet  12737