Theorem simp3lr 1068

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

Assertion

Ref	Expression
simp3lr

Proof of Theorem simp3lr

Step	Hyp	Ref	Expression
1		simplr 755	. 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  btwnconn1lem4  29740  pellex  30771  jm2.27  30950  athgt  35180  2llnjN  35291  4atlem12b  35335  lncmp  35507  cdlema2N  35516  cdleme21ct  36055  cdleme24  36078  cdleme27a  36093  cdleme28  36099  cdleme42b  36204  cdlemf  36289  dihlsscpre  36961  dihord4  36985  dihord5apre  36989

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