Theorem ancom2s 650

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 593	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  661  sotr2  5561  somin2  6087  f1elima  7203  f1imaeq  7205  soisoi  7268  isosolem  7287  xpexr2  7855  smoword  8292  unxpdomlem3  9148  fiming  9390  fiinfg  9391  sornom  10174  fin1a2s  10311  mul4r  11288  mulsub  11566  leltadd  11607  ltord1  11649  leord1  11650  eqord1  11651  divmul24  11831  expcan  14082  ltexp2  14083  bhmafibid2  15382  fsum  15633  fprod  15854  isprm5  16624  ramub  16931  setcinv  18003  grpidpropd  18576  gsumpropd2lem  18593  cmnpropd  19709  gsumcom3  19896  unitpropd  20341  lidl1el  21169  1marepvmarrepid  22496  1marepvsma1  22504  ordtrest2  23125  filuni  23806  haustsms2  24058  blcomps  24314  blcom  24315  metnrmlem3  24783  cnmpopc  24855  icoopnst  24869  icccvx  24881  equivcfil  25232  volcn  25540  dvmptfsum  25912  cxple  26637  cxple3  26643  om2noseqlt2  28236  om2noseqf1o  28237  uhgr2edg  29193  lnosub  30746  chirredlem2  32378  metider  33914  ordtrest2NEW  33943  fsum2dsub  34627  finxpreclem2  37441  fin2so  37653  cover2  37761  filbcmb  37786  isdrngo2  38004  crngohomfo  38052  unichnidl  38077  cdleme50eq  40646  dvhvaddcomN  41201  ismrc  42799  prproropf1olem4  47611  pgnbgreunbgrlem4  48224