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

Theorem ancom2s 802
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 449 . 2
2 an12s.1 . 2
31, 2sylan2 474 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  an42s  827  sotr2  4834  somin2  5410  f1elima  6171  f1imaeq  6173  soisoi  6224  isosolem  6243  xpexr2  6741  2ndconst  6889  smoword  7056  unxpdomlem3  7746  sornom  8678  fin1a2s  8815  mulsub  10024  leltadd  10061  ltord1  10104  leord1  10105  eqord1  10106  divmul24  10273  expcan  12218  ltexp2  12219  fsum  13542  fprod  13748  isprm5  14253  ramub  14531  setcinv  15417  grpidpropd  15888  gsumpropd2lem  15900  cmnpropd  16807  unitpropd  17346  lidl1el  17866  gsumcom3  18901  1marepvmarrepid  19077  1marepvsma1  19085  ordtrest2  19705  filuni  20386  haustsms2  20635  blcomps  20896  blcom  20897  metnrmlem3  21365  cnmpt2pc  21428  icoopnst  21439  icccvx  21450  equivcfil  21738  volcn  22015  dvmptfsum  22376  cxple  23076  cxple3  23082  subgoablo  25313  ghabloOLD  25371  lnosub  25674  chirredlem2  27310  bhmafibid2  27633  metider  27873  ordtrest2NEW  27905  fin2so  30040  cover2  30204  filbcmb  30231  isdrngo2  30361  crngohomfo  30403  unichnidl  30428  ismrc  30633  cdleme50eq  36267  dvhvaddcomN  36823
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 185  df-an 371
  Copyright terms: Public domain W3C validator