Theorem simpl21 1074

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

Assertion

Ref	Expression
simpl21

Proof of Theorem simpl21

Step	Hyp	Ref	Expression
1		simp21 1029	. 2
2	1	adantr 465	1

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

This theorem is referenced by:  brbtwn2  24208  ax5seglem3a  24233  ax5seg  24241  axpasch  24244  axeuclid  24266  br8d  27463  br8  29185  cgrextend  29658  segconeq  29660  trisegint  29678  ifscgr  29694  cgrsub  29695  cgrxfr  29705  lineext  29726  seglecgr12im  29760  segletr  29764  lineunray  29797  lineelsb2  29798  cvrcmp  35008  cvlatexch3  35063  cvlsupr2  35068  atexchcvrN  35164  3dim1  35191  3dim2  35192  ps-1  35201  ps-2  35202  3atlem3  35209  3atlem5  35211  lplnnle2at  35265  lplnllnneN  35280  2llnjaN  35290  4atlem3  35320  4atlem10b  35329  4atlem12  35336  2llnma3r  35512  paddasslem4  35547  paddasslem7  35550  paddasslem8  35551  paddasslem12  35555  paddasslem13  35556  pmodlem1  35570  pmodlem2  35571  llnexchb2lem  35592  4atex2  35801  ltrnatlw  35908  trlval4  35913  arglem1N  35915  cdlemd4  35926  cdlemd5  35927  cdleme0moN  35950  cdleme16  36010  cdleme20  36050  cdleme21j  36062  cdleme21k  36064  cdleme27N  36095  cdleme28c  36098  cdleme43fsv1snlem  36146  cdleme38n  36190  cdleme40n  36194  cdleme41snaw  36202  cdlemg6c  36346  cdlemg8c  36355  cdlemg8  36357  cdlemg12e  36373  cdlemg16  36383  cdlemg16ALTN  36384  cdlemg16z  36385  cdlemg16zz  36386  cdlemg18a  36404  cdlemg20  36411  cdlemg22  36413  cdlemg37  36415  cdlemg27b  36422  cdlemg31d  36426  cdlemg33  36437  cdlemg38  36441  cdlemg44b  36458  cdlemk38  36641  cdlemk35s-id  36664  cdlemk39s-id  36666  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