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

Theorem ancomsd 454
 Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
Hypothesis
Ref Expression
ancomsd.1
Assertion
Ref Expression
ancomsd

Proof of Theorem ancomsd
StepHypRef Expression
1 ancom 450 . 2
2 ancomsd.1 . 2
31, 2syl5bi 217 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  sylan2d  482  mpand  675  anabsi6  818  ralcom2  3022  ralxfrd  4666  somo  4839  wereu2  4881  ordtr3  4928  poirr2  5396  smoel  7050  cfub  8650  cofsmo  8670  grudomon  9216  axpre-sup  9567  leltadd  10061  lemul12b  10424  lbzbi  11199  injresinj  11926  abslt  13147  absle  13148  o1lo1  13360  o1co  13409  rlimno1  13476  znnenlem  13945  dvdssub2  14023  lublecllem  15618  f1omvdco2  16473  ptpjpre1  20072  iocopnst  21440  ovolicc2lem4  21931  itg2le  22146  ulmcau  22790  cxpeq0  23059  pntrsumbnd2  23752  cvcon3  27203  atexch  27300  abfmpeld  27492  wsuclem  29381  nofulllem5  29466  btwntriv2  29662  btwnexch3  29670  finixpnum  30038  fin2solem  30039  ltflcei  30043  itg2addnclem  30066  unirep  30203  prter2  30622  incssnn0  30643  eldioph4b  30745  fphpdo  30751  pellexlem5  30769  pm14.24  31339  aacllem  33216  cvrcon3b  35002 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