Theorem simpr1l 1053

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpr1l

Proof of Theorem simpr1l

Step	Hyp	Ref	Expression
1		simp1l 1020	. 2
2	1	adantl 466	1

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