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

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

Proof of Theorem simpl33
StepHypRef Expression
1 simp33 996 . 2
21adantr 453 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  /\w3a 937
This theorem is referenced by:  br8  25639  ax5seglem3a  26129  ax5seg  26137  cgrextend  26202  segconeq  26204  trisegint  26222  ifscgr  26238  cgrsub  26239  btwnxfr  26250  seglecgr12im  26304  segletr  26308  atbtwn  30639  4atlem10b  30798  4atlem11  30802  4atlem12  30805  2lplnj  30813  paddasslem4  31016  paddasslem7  31019  pmodlem1  31039  4atex2  31270  trlval3  31380  arglem1N  31383  cdleme0moN  31418  cdleme20  31517  cdleme21j  31529  cdleme28c  31565  cdleme38n  31657  cdlemg6c  31813  cdlemg6  31816  cdlemg7N  31819  cdlemg16  31850  cdlemg16ALTN  31851  cdlemg16zz  31853  cdlemg20  31878  cdlemg22  31880  cdlemg37  31882  cdlemg31d  31893  cdlemg29  31898  cdlemg33b  31900  cdlemg33  31904  cdlemg46  31928  cdlemk25-3  32097
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator