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

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

Proof of Theorem simpl33
StepHypRef Expression
1 simp33 1034 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  ax5seglem3a  24233  ax5seg  24241  br8d  27463  br8  29185  cgrextend  29658  segconeq  29660  trisegint  29678  ifscgr  29694  cgrsub  29695  btwnxfr  29706  seglecgr12im  29760  segletr  29764  atbtwn  35170  4atlem10b  35329  4atlem11  35333  4atlem12  35336  2lplnj  35344  paddasslem4  35547  paddasslem7  35550  pmodlem1  35570  4atex2  35801  trlval3  35912  arglem1N  35915  cdleme0moN  35950  cdleme20  36050  cdleme21j  36062  cdleme28c  36098  cdleme38n  36190  cdlemg6c  36346  cdlemg6  36349  cdlemg7N  36352  cdlemg16  36383  cdlemg16ALTN  36384  cdlemg16zz  36386  cdlemg20  36411  cdlemg22  36413  cdlemg37  36415  cdlemg31d  36426  cdlemg29  36431  cdlemg33b  36433  cdlemg33  36437  cdlemg46  36461  cdlemk25-3  36630
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