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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1029 . 2
213ad2ant1 1017 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  ax5seglem3  24234  axpasch  24244  exatleN  35128  ps-2b  35206  3atlem1  35207  3atlem2  35208  3atlem4  35210  3atlem5  35211  3atlem6  35212  2llnjaN  35290  4atlem12b  35335  2lplnja  35343  dalempea  35350  dath2  35461  lneq2at  35502  llnexchb2  35593  dalawlem1  35595  osumcllem7N  35686  lhpexle3lem  35735  cdleme26ee  36086  cdlemg34  36438  cdlemg36  36440  cdlemj1  36547  cdlemj2  36548  cdlemk23-3  36628  cdlemk25-3  36630  cdlemk26b-3  36631  cdlemk26-3  36632  cdlemk27-3  36633  cdleml3N  36704
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