Theorem simp-4r 768

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

Assertion

Ref	Expression
simp-4r

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		simpllr 760	. 2
2	1	adantr 465	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  simp-5r  770  tfrlem1  7064  injresinj  11926  swrdsymbeq  12672  reuccats1  12706  prdsval  14852  catcocl  15082  catass  15083  catpropd  15104  cidpropd  15105  monpropd  15132  subccocl  15214  funcco  15240  funcpropd  15269  fucpropd  15346  xpcpropd  15477  curf2ndf  15516  drsdirfi  15567  mhmmnd  16192  gsmsymgreqlem2  16456  dfod2  16586  ghmcmn  16840  psgndif  18638  dmatscmcl  19005  smatvscl  19026  cpmatmcllem  19219  pm2mpmhmlem2  19320  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  neitr  19681  1stcrest  19954  dissnref  20029  dissnlocfin  20030  neitx  20108  tgqtop  20213  ptcmplem3  20554  trust  20732  utoptop  20737  restutopopn  20741  ustuqtop2  20745  ustuqtop4  20747  utop3cls  20754  isucn2  20782  met1stc  21024  prdsxmslem2  21032  metustexhalfOLD  21066  metustexhalf  21067  cfilucfilOLD  21072  cfilucfil  21073  metucnOLD  21091  metucn  21092  aannenlem1  22724  ulmuni  22787  pntpbnd  23773  pntlem3  23794  istrkgb  23852  tgbtwndiff  23897  tgifscgr  23900  tgbtwnconn1lem3  23961  tgbtwnconn1  23962  legov  23972  legtrd  23976  legtri3  23977  ltgseg  23982  legso  23985  tglinethru  24016  tglnpt2  24021  colline  24030  miriso  24050  midexlem  24069  perpneq  24091  isperp2  24092  footex  24095  midex  24111  opphllem3  24121  opphl  24125  lnopp2hpgb  24132  lmieu  24150  f1otrg  24174  axcontlem2  24268  pthdepisspth  24576  usgra2adedgwlkonALT  24616  clwlkfclwwlk  24844  2sqmo  27637  ressprs  27643  omndmul2  27702  isarchi3  27731  isarchiofld  27807  fimaproj  27836  txomap  27837  qtophaus  27839  pstmxmet  27876  sqsscirc1  27890  lmxrge0  27934  esumcst  28071  esumfsup  28076  signstfvneq0  28529  afsval  28551  lgamucov  28580  mblfinlem3  30053  itg2addnclem  30066  nn0prpwlem  30140  sstotbnd2  30270  prdstotbnd  30290  diophren  30747  rencldnfilem  30754  pellex  30771  pell1234qrdich  30797  pell1qrgap  30810  pellfundex  30822  limcrecl  31635  limcleqr  31650  0ellimcdiv  31655  limclner  31657  icccncfext  31690  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  fourierdlem50  31939  fourierdlem51  31940  fourierdlem80  31969  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  initoeu2lem1  32620  iunconlem2  33735  lcfl8  37229

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