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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1021 . 2
213ad2ant1 1009 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 965
This theorem is referenced by:  ax5seglem3  23646  axpasch  23656  exatleN  33899  ps-2b  33977  3atlem1  33978  3atlem2  33979  3atlem4  33981  3atlem5  33982  3atlem6  33983  2llnjaN  34061  4atlem12b  34106  2lplnja  34114  dalempea  34121  dath2  34232  lneq2at  34273  llnexchb2  34364  dalawlem1  34366  osumcllem7N  34457  lhpexle3lem  34506  cdleme26ee  34855  cdlemg34  35207  cdlemg36  35209  cdlemj1  35316  cdlemj2  35317  cdlemk23-3  35397  cdlemk25-3  35399  cdlemk26b-3  35400  cdlemk26-3  35401  cdlemk27-3  35402  cdleml3N  35473
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 967
  Copyright terms: Public domain W3C validator