Theorem simpr2l 1055

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

Assertion

Ref	Expression
simpr2l

Proof of Theorem simpr2l

Step	Hyp	Ref	Expression
1		simp2l 1022	. 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  kerf1hrm  17392  nllyidm  19990  ax5seg  24241  segconeq  29660  ifscgr  29694  brofs2  29727  brifs2  29728  idinside  29734  btwnconn1lem8  29744  btwnconn1lem12  29748  segcon2  29755  segletr  29764  outsidele  29782  estrccatid  32638  lplnexllnN  35288  paddasslem9  35552  pmodlem2  35571  lhp2lt  35725  cdlemc3  35918  cdlemc4  35919  cdlemd1  35923  cdleme3b  35954  cdleme3c  35955  cdleme42ke  36211  cdlemg4c  36338

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