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

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

Proof of Theorem simp1ll
StepHypRef Expression
1 simpll 753 . 2
213ad2ant1 1017 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  lspsolvlem  17788  1marepvsma1  19085  mdetunilem8  19121  madutpos  19144  ax5seg  24241  rabfodom  27404  measinblem  28191  btwnconn1lem2  29738  btwnconn1lem13  29749  limccog  31626  icccncfext  31690  stoweidlem31  31813  stoweidlem34  31816  stoweidlem49  31831  stoweidlem57  31839  athgt  35180  llnle  35242  lplnle  35264  lhpexle1  35732  lhpj1  35746  lhpat3  35770  ltrncnv  35870  cdleme16aN  35984  tendoicl  36522  cdlemk55b  36686  dihatexv  37065  dihglblem6  37067
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