Theorem simp-4l 767

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-4l

Proof of Theorem simp-4l

Step	Hyp	Ref	Expression
1		simplll 759	. 2
2	1	adantr 465	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  simp-5l  769  marypha1lem  7913  acndom2  8456  ttukeylem6  8915  fpwwe2lem12  9040  reuccats1  12706  ramcl  14547  gsmsymgreqlem2  16456  dfod2  16586  pgpfi  16625  ghmcyg  16898  psgndif  18638  scmatmulcl  19020  cpmatmcllem  19219  neiptoptop  19632  cncnp  19781  subislly  19982  ptcnplem  20122  pthaus  20139  xkohaus  20154  kqreglem1  20242  cnextcn  20567  qustgplem  20619  trust  20732  utoptop  20737  restutopopn  20741  ustuqtop2  20745  ustuqtop3  20746  utop3cls  20754  utopreg  20755  isucn2  20782  met1stc  21024  metustsymOLD  21064  metustsym  21065  metustOLD  21070  metust  21071  metuel2  21082  xrge0tsms  21339  xmetdcn2  21342  nmoleub2lem2  21599  iscfil2  21705  iscfil3  21712  dvmptfsum  22376  dvlip2  22396  aannenlem1  22724  ulm2  22780  ulmuni  22787  mtestbdd  22800  efopn  23039  dchrptlem1  23539  pntpbnd  23773  pntibnd  23778  legval  23971  f1otrg  24174  f1otrge  24175  pthdepisspth  24576  usgra2adedgwlkonALT  24616  cusconngra  24676  clwlkisclwwlklem2a4  24784  xrofsup  27582  ressprs  27643  omndmul2  27702  isarchi3  27731  archirngz  27733  lmodslmd  27747  xrge0tsmsd  27775  suborng  27805  isarchiofld  27807  sqsscirc1  27890  lmxrge0  27934  lmdvg  27935  esumfsup  28076  esumcvg  28092  ddemeas  28208  btwnconn1lem13  29749  mblfinlem3  30053  mblfinlem4  30054  ftc1anclem7  30096  ftc1anc  30098  prdstotbnd  30290  rencldnfilem  30754  pellex  30771  pellfundex  30822  dvdsacongtr  30922  fnchoice  31404  climsuse  31614  addlimc  31654  0ellimcdiv  31655  limclner  31657  icccncfext  31690  dvnprodlem3  31745  fourierdlem12  31901  fourierdlem34  31923  fourierdlem50  31939  fourierdlem80  31969  fourierdlem81  31970  fourierdlem87  31976  etransclem35  32052  usgra2pth  32354  initoeu2lem1  32620  uzlidlring  32735  2zlidl  32740  ltrnid  35859

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