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

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

Proof of Theorem simp1l1
StepHypRef Expression
1 simpl1 999 . 2
213ad2ant1 1017 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  mapxpen  7703  lsmcv  17787  archiabl  27742  trisegint  29678  linethru  29803  hlrelat3  35136  cvrval3  35137  cvrval4N  35138  2atlt  35163  atbtwnex  35172  1cvratlt  35198  atcvrlln2  35243  atcvrlln  35244  2llnmat  35248  lplnexllnN  35288  lvolnlelpln  35309  lnjatN  35504  lncvrat  35506  lncmp  35507  cdlemd9  35931  dihord5b  36986  dihmeetALTN  37054  dih1dimatlem0  37055  mapdrvallem2  37372
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