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

Theorem simpr1l 1053
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpr1l

Proof of Theorem simpr1l
StepHypRef Expression
1 simp1l 1020 . 2
21adantl 466 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 973 This theorem is referenced by:  oppccatid  15114  subccatid  15215  setccatid  15411  catccatid  15429  xpccatid  15457  gsmsymgreqlem1  16455  dmdprdsplit  17096  neiptopnei  19633  neitr  19681  neitx  20108  tx1stc  20151  utop3cls  20754  metustsymOLD  21064  metustsym  21065  ax5seg  24241  frgrawopreg  25049  esumpcvgval  28084  ifscgr  29694  brofs2  29727  brifs2  29728  btwnconn1lem8  29744  btwnconn1lem12  29748  seglecgr12im  29760  stoweidlem60  31842  estrccatid  32638  lhp2lt  35725  cdlemd1  35923  cdleme3b  35954  cdleme3c  35955  cdleme3e  35957  cdlemf2  36288  cdlemg4c  36338  cdlemn11pre  36937  dihmeetlem12N  37045 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  df-3an 975
 Copyright terms: Public domain W3C validator