Theorem simpl23 1076

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

Assertion

Ref	Expression
simpl23

Proof of Theorem simpl23

Step	Hyp	Ref	Expression
1		simp23 1031	. 2
2	1	adantr 465	1

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

This theorem is referenced by:  mulgdirlem  16166  brbtwn2  24208  ax5seglem3a  24233  ax5seg  24241  axpasch  24244  axeuclid  24266  br8d  27463  br8  29185  cgrextend  29658  segconeq  29660  segconeu  29661  trisegint  29678  ifscgr  29694  cgrsub  29695  cgrxfr  29705  lineext  29726  seglecgr12im  29760  segletr  29764  lineunray  29797  lineelsb2  29798  cvrcmp  35008  cvlsupr2  35068  atcvrj2b  35156  atexchcvrN  35164  3atlem3  35209  3atlem5  35211  lplnnle2at  35265  lplnllnneN  35280  4atlem3  35320  4atlem10b  35329  4atlem12  35336  2llnma3r  35512  paddasslem4  35547  paddasslem7  35550  paddasslem8  35551  paddasslem12  35555  paddasslem13  35556  paddasslem15  35558  pmodlem1  35570  pmodlem2  35571  atmod1i1m  35582  llnexchb2lem  35592  4atex2  35801  ltrnatlw  35908  arglem1N  35915  cdlemd4  35926  cdlemd5  35927  cdleme16  36010  cdleme20  36050  cdleme21k  36064  cdleme27N  36095  cdleme28c  36098  cdleme43fsv1snlem  36146  cdleme38n  36190  cdleme40n  36194  cdleme41snaw  36202  cdlemg6c  36346  cdlemg8c  36355  cdlemg8  36357  cdlemg12e  36373  cdlemg16ALTN  36384  cdlemg16zz  36386  cdlemg18a  36404  cdlemg20  36411  cdlemg22  36413  cdlemg37  36415  cdlemg31d  36426  cdlemg33  36437  cdlemg38  36441  cdlemg44b  36458  cdlemk33N  36635  cdlemk34  36636  cdlemk38  36641  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk53b  36682  cdlemk53  36683  cdlemk55  36687  cdlemk35u  36690  cdlemk55u  36692  cdleml3N  36704  cdlemn11pre  36937

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