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

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

Proof of Theorem simpl33
StepHypRef Expression
1 simp33 995 . 2
21adantr 452 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 359  /\w3a 936
This theorem is referenced by:  br8  25371  ax5seglem3a  25861  ax5seg  25869  cgrextend  25934  segconeq  25936  trisegint  25954  ifscgr  25970  cgrsub  25971  btwnxfr  25982  seglecgr12im  26036  segletr  26040  atbtwn  30180  4atlem10b  30339  4atlem11  30343  4atlem12  30346  2lplnj  30354  paddasslem4  30557  paddasslem7  30560  pmodlem1  30580  4atex2  30811  trlval3  30921  arglem1N  30924  cdleme0moN  30959  cdleme20  31058  cdleme21j  31070  cdleme28c  31106  cdleme38n  31198  cdlemg6c  31354  cdlemg6  31357  cdlemg7N  31360  cdlemg16  31391  cdlemg16ALTN  31392  cdlemg16zz  31394  cdlemg20  31419  cdlemg22  31421  cdlemg37  31423  cdlemg31d  31434  cdlemg29  31439  cdlemg33b  31441  cdlemg33  31445  cdlemg46  31469  cdlemk25-3  31638
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator