Theorem ancom2s 651

Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
an12s.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
ancom2s	⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)

Proof of Theorem ancom2s

Step	Hyp	Ref	Expression
1		pm3.22 459	. 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 594	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  an42s  662  sotr2  5564  somin2  6090  f1elima  7209  f1imaeq  7211  soisoi  7274  isosolem  7293  xpexr2  7861  smoword  8297  unxpdomlem3  9159  fiming  9404  fiinfg  9405  sornom  10188  fin1a2s  10325  mul4r  11303  mulsub  11581  leltadd  11622  ltord1  11664  leord1  11665  eqord1  11666  divmul24  11846  expcan  14093  ltexp2  14094  bhmafibid2  15393  fsum  15644  fprod  15865  isprm5  16635  ramub  16942  setcinv  18015  grpidpropd  18588  gsumpropd2lem  18605  cmnpropd  19724  gsumcom3  19911  unitpropd  20355  lidl1el  21183  1marepvmarrepid  22518  1marepvsma1  22526  ordtrest2  23147  filuni  23828  haustsms2  24080  blcomps  24336  blcom  24337  metnrmlem3  24805  cnmpopc  24873  icoopnst  24884  icccvx  24895  equivcfil  25244  volcn  25551  dvmptfsum  25920  cxple  26644  cxple3  26650  om2noseqlt2  28280  om2noseqf1o  28281  uhgr2edg  29265  lnosub  30819  chirredlem2  32451  metider  34044  ordtrest2NEW  34073  fsum2dsub  34757  finxpreclem2  37702  fin2so  37919  cover2  38027  filbcmb  38052  isdrngo2  38270  crngohomfo  38318  unichnidl  38343  cdleme50eq  40978  dvhvaddcomN  41533  ismrc  43132  prproropf1olem4  47940  pgnbgreunbgrlem4  48553