Theorem simp2ll 1063

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

Assertion

Ref	Expression
simp2ll

Proof of Theorem simp2ll

Step	Hyp	Ref	Expression
1		simpll 753	. 2
2	1	3ad2ant2 1018	1

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

This theorem is referenced by:  tfrlem5  7068  omeu  7253  4sqlem18  14480  vdwlem10  14508  0catg  15084  mvrf1  18081  mdetuni0  19123  mdetmul  19125  tsmsxp  20657  ax5seglem3  24234  btwnconn1lem1  29737  btwnconn1lem2  29738  btwnconn1lem3  29739  btwnconn1lem12  29748  btwnconn1lem13  29749  pellex  30771  expmordi  30883  lshpkrlem6  34840  athgt  35180  2llnjN  35291  dalaw  35610  lhpmcvr4N  35750  cdlemb2  35765  4atexlemex6  35798  cdlemd7  35929  cdleme01N  35946  cdleme02N  35947  cdleme0ex1N  35948  cdleme0ex2N  35949  cdleme7aa  35967  cdleme7c  35970  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme7  35974  cdleme11a  35985  cdleme20k  36045  cdleme27cl  36092  cdleme42e  36205  cdleme42h  36208  cdleme42i  36209  cdlemf  36289  cdlemg2kq  36328  cdlemg2m  36330  cdlemg8a  36353  cdlemg11aq  36364  cdlemg10c  36365  cdlemg11b  36368  cdlemg17a  36387  cdlemg31b0N  36420  cdlemg31c  36425  cdlemg33c0  36428  cdlemg41  36444  cdlemh2  36542  cdlemn9  36932  dihglbcpreN  37027  dihmeetlem3N  37032  dihmeetlem13N  37046

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