Theorem simpr3l 1057

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

Assertion

Ref	Expression
simpr3l

Proof of Theorem simpr3l

Step	Hyp	Ref	Expression
1		simp3l 1024	. 2
2	1	adantl 466	1

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

This theorem is referenced by:  ax5seg  24241  axcont  24279  segconeq  29660  idinside  29734  btwnconn1lem10  29746  segletr  29764  stoweidlem56  31838  cdlemc3  35918  cdlemc4  35919  cdleme1  35952  cdleme2  35953  cdleme3b  35954  cdleme3c  35955  cdleme3e  35957  cdleme27a  36093

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