Theorem ancom2s 641

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 452	. 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 587	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  an42s  652  sotr2  5260  somin2  5747  f1elima  6746  f1imaeq  6748  soisoi  6804  isosolem  6823  xpexr2  7340  smoword  7700  unxpdomlem3  8406  fiming  8644  fiinfg  8645  sornom  9385  fin1a2s  9522  mulsub  10763  leltadd  10802  ltord1  10844  leord1  10845  eqord1  10846  divmul24  11019  expcan  13163  ltexp2  13164  fsum  14789  fprod  15005  isprm5  15749  ramub  16047  setcinv  17051  grpidpropd  17573  gsumpropd2lem  17585  cmnpropd  18514  unitpropd  19010  lidl1el  19538  gsumcom3  20527  1marepvmarrepid  20704  1marepvsma1  20712  ordtrest2  21334  filuni  22014  haustsms2  22265  blcomps  22523  blcom  22524  metnrmlem3  22989  cnmpt2pc  23052  icoopnst  23063  icccvx  23074  equivcfil  23422  volcn  23711  dvmptfsum  24076  cxple  24779  cxple3  24785  uhgr2edg  26433  lnosub  28131  chirredlem2  29767  bhmafibid2  30153  metider  30445  ordtrest2NEW  30477  fsum2dsub  31197  finxpreclem2  33717  fin2so  33877  cover2  33988  filbcmb  34015  isdrngo2  34236  crngohomfo  34284  unichnidl  34309  cdleme50eq  36554  dvhvaddcomN  37109  ismrc  38038