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  5622  somin2  6142  f1elima  7272  f1imaeq  7274  soisoi  7334  isosolem  7353  xpexr2  7926  smoword  8386  unxpdomlem3  9276  fiming  9522  fiinfg  9523  sornom  10301  fin1a2s  10438  mul4r  11414  mulsub  11688  leltadd  11729  ltord1  11771  leord1  11772  eqord1  11773  divmul24  11949  expcan  14167  ltexp2  14168  bhmafibid2  15447  fsum  15700  fprod  15919  isprm5  16679  ramub  16983  setcinv  18080  grpidpropd  18623  gsumpropd2lem  18640  cmnpropd  19755  gsumcom3  19942  unitpropd  20365  lidl1el  21131  1marepvmarrepid  22517  1marepvsma1  22525  ordtrest2  23148  filuni  23829  haustsms2  24081  blcomps  24339  blcom  24340  metnrmlem3  24817  cnmpopc  24889  icoopnst  24903  icccvx  24915  equivcfil  25267  volcn  25575  dvmptfsum  25947  cxple  26669  cxple3  26675  om2noseqlt2  28217  om2noseqf1o  28218  uhgr2edg  29087  lnosub  30635  chirredlem2  32267  metider  33610  ordtrest2NEW  33639  fsum2dsub  34354  finxpreclem2  36984  fin2so  37195  cover2  37303  filbcmb  37328  isdrngo2  37546  crngohomfo  37594  unichnidl  37619  cdleme50eq  40128  dvhvaddcomN  40683  ismrc  42233  prproropf1olem4  46953

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

OSZAR »