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

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

Proof of Theorem simpr2l
StepHypRef Expression
1 simp2l 1022 . 2
 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  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