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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1025 . 2
213ad2ant1 1017 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  pceu  14370  axpasch  24244  addlimc  31654  3dimlem4  35188  3atlem4  35210  llncvrlpln2  35281  2lplnja  35343  lhpmcvr5N  35751  4atexlemswapqr  35787  4atexlemnclw  35794  trlval2  35888  cdleme21h  36060  cdleme24  36078  cdleme26ee  36086  cdleme26f  36089  cdleme26f2  36091  cdlemf1  36287  cdlemg16ALTN  36384  cdlemg17iqN  36400  cdlemg27b  36422  trlcone  36454  cdlemg48  36463  tendocan  36550  cdlemk26-3  36632  cdlemk27-3  36633  cdlemk28-3  36634  cdlemk37  36640  cdlemky  36652  cdlemk11ta  36655  cdlemkid3N  36659  cdlemk11t  36672  cdlemk46  36674  cdlemk47  36675  cdlemk51  36679  cdlemk52  36680  cdleml4N  36705  dihmeetlem1N  37017  dihmeetlem20N  37053  mapdpglem32  37432
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