Theorem simpr1r 1054

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

Assertion

Ref	Expression
simpr1r

Proof of Theorem simpr1r

Step	Hyp	Ref	Expression
1		simp1r 1021	. 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  neitr  19681  neitx  20108  tx1stc  20151  utop3cls  20754  metustsymOLD  21064  metustsym  21065  frgrawopreg  25049  archiabllem1  27737  esumpcvgval  28084  ifscgr  29694  btwnconn1lem8  29744  btwnconn1lem11  29747  btwnconn1lem12  29748  segletr  29764  broutsideof3  29776  stoweidlem60  31842  estrccatid  32638  lhp2lt  35725  cdlemf2  36288  cdlemn11pre  36937

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