Theorem simpl32 1078

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl32

Proof of Theorem simpl32

Step	Hyp	Ref	Expression
1		simp32 1033	. 2
2	1	adantr 465	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  mulmarep1gsum2  19076  tsmsxp  20657  ax5seg  24241  br8d  27463  br8  29185  cgrextend  29658  segconeq  29660  trisegint  29678  ifscgr  29694  cgrsub  29695  btwnxfr  29706  seglecgr12im  29760  segletr  29764  initoeu2lem2  32621  exatleN  35128  atbtwn  35170  3dim1  35191  3dim2  35192  2llnjaN  35290  4atlem10b  35329  4atlem11  35333  4atlem12  35336  2lplnj  35344  cdlemb  35518  paddasslem4  35547  pmodlem1  35570  4atex2  35801  trlval3  35912  arglem1N  35915  cdleme0moN  35950  cdleme17b  36012  cdleme20  36050  cdleme21j  36062  cdleme28c  36098  cdleme35h2  36183  cdleme38n  36190  cdlemg6c  36346  cdlemg6  36349  cdlemg7N  36352  cdlemg11a  36363  cdlemg12e  36373  cdlemg16  36383  cdlemg16ALTN  36384  cdlemg16zz  36386  cdlemg20  36411  cdlemg22  36413  cdlemg37  36415  cdlemg31d  36426  cdlemg29  36431  cdlemg33b  36433  cdlemg33  36437  cdlemg39  36442  cdlemg42  36455  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