Theorem ancom2s 648

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  an42s  659  sotr2  5616  somin2  6136  f1elima  7268  f1imaeq  7270  soisoi  7331  isosolem  7350  xpexr2  7923  smoword  8383  unxpdomlem3  9273  fiming  9519  fiinfg  9520  sornom  10298  fin1a2s  10435  mul4r  11411  mulsub  11685  leltadd  11726  ltord1  11768  leord1  11769  eqord1  11770  divmul24  11946  expcan  14163  ltexp2  14164  bhmafibid2  15443  fsum  15696  fprod  15915  isprm5  16675  ramub  16979  setcinv  18076  grpidpropd  18619  gsumpropd2lem  18636  cmnpropd  19748  gsumcom3  19935  unitpropd  20358  lidl1el  21124  1marepvmarrepid  22493  1marepvsma1  22501  ordtrest2  23124  filuni  23805  haustsms2  24057  blcomps  24315  blcom  24316  metnrmlem3  24793  cnmpopc  24865  icoopnst  24879  icccvx  24891  equivcfil  25243  volcn  25551  dvmptfsum  25923  cxple  26645  cxple3  26651  om2noseqlt2  28193  om2noseqf1o  28194  uhgr2edg  29063  lnosub  30611  chirredlem2  32243  metider  33551  ordtrest2NEW  33580  fsum2dsub  34295  finxpreclem2  36925  fin2so  37136  cover2  37244  filbcmb  37269  isdrngo2  37487  crngohomfo  37535  unichnidl  37560  cdleme50eq  40069  dvhvaddcomN  40624  ismrc  42185  prproropf1olem4  46908

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »