MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancom2s Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm3.22 458 . 2 ((𝜒𝜓) → (𝜓𝜒))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 591 1 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator
OSZAR »