Theorem simp3ll 1067

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

Assertion

Ref	Expression
simp3ll

Proof of Theorem simp3ll

Step	Hyp	Ref	Expression
1		simpll 753	. 2
2	1	3ad2ant3 1019	1

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

This theorem is referenced by:  f1oiso2  6248  omeu  7253  ntrivcvgmul  13711  tsmsxp  20657  tgqioo  21305  ovolunlem2  21909  plyadd  22614  plymul  22615  coeeu  22622  tghilbert1_2  24018  btwnconn1lem2  29738  btwnconn1lem3  29739  btwnconn1lem12  29748  pellex  30771  jm2.27  30950  athgt  35180  2llnjN  35291  4atlem12b  35335  lncmp  35507  cdlema2N  35516  cdlemc2  35917  cdleme5  35965  cdleme11a  35985  cdleme21ct  36055  cdleme21  36063  cdleme22eALTN  36071  cdleme24  36078  cdleme27cl  36092  cdleme27a  36093  cdleme28  36099  cdleme36a  36186  cdleme42b  36204  cdleme48fvg  36226  cdlemf  36289  cdlemk39  36642  cdlemkid1  36648  dihlsscpre  36961  dihord4  36985  dihord5apre  36989  dihmeetlem20N  37053  mapdh9a  37517

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