Theorem simp3rl 1069

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

Assertion

Ref	Expression
simp3rl

Proof of Theorem simp3rl

Step	Hyp	Ref	Expression
1		simprl 756	. 2
2	1	3ad2ant3 1019	1

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

This theorem is referenced by:  omeu  7253  hashbclem  12501  ntrivcvgmul  13711  tsmsxp  20657  tgqioo  21305  ovolunlem2  21909  plyadd  22614  plymul  22615  coeeu  22622  tghilbert1_2  24018  gxmul  25280  cvmlift2lem10  28757  btwnconn1lem1  29737  btwnconn1lem2  29738  btwnconn1lem12  29748  jm2.27  30950  lplnexllnN  35288  2llnjN  35291  4atlem12b  35335  lplncvrlvol2  35339  lncmp  35507  cdlema2N  35516  cdlemc2  35917  cdleme11a  35985  cdleme22eALTN  36071  cdleme24  36078  cdleme27a  36093  cdleme27N  36095  cdleme28  36099  cdlemefs29bpre0N  36142  cdlemefs29bpre1N  36143  cdlemefs29cpre1N  36144  cdlemefs29clN  36145  cdlemefs32fvaN  36148  cdlemefs32fva1  36149  cdleme36m  36187  cdleme39a  36191  cdleme17d3  36222  cdleme50trn2  36277  cdlemg36  36440  cdlemj3  36549  cdlemkfid1N  36647  cdlemkid1  36648  cdlemk19ylem  36656  cdlemk19xlem  36668  dihlsscpre  36961  dihord4  36985  dihatlat  37061  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