Theorem simp-4r 807

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

Assertion

Ref	Expression
simp-4r	|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		simpllr 799	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
2	1	adantr 481	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  simp-5r  809  tfrlem1  7472  injresinj  12589  reuccats1  13480  prdsval  16115  catcocl  16346  catass  16347  catpropd  16369  cidpropd  16370  monpropd  16397  subccocl  16505  funcco  16531  funcpropd  16560  fucpropd  16637  initoeu2lem1  16664  xpcpropd  16848  curf2ndf  16887  drsdirfi  16938  mhmmnd  17537  gsmsymgreqlem2  17851  dfod2  17981  ghmcmn  18237  psgndif  19948  dmatscmcl  20309  smatvscl  20330  cpmatmcllem  20523  pm2mpmhmlem2  20624  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  neitr  20984  1stcrest  21256  dissnref  21331  dissnlocfin  21332  neitx  21410  tgqtop  21515  ptcmplem3  21858  trust  22033  utoptop  22038  restutopopn  22042  ustuqtop2  22046  ustuqtop4  22048  utop3cls  22055  isucn2  22083  met1stc  22326  prdsxmslem2  22334  metustexhalf  22361  cfilucfil  22364  metucn  22376  aannenlem1  24083  ulmuni  24146  lgamucov  24764  pntpbnd  25277  pntlem3  25298  istrkgb  25354  tgbtwndiff  25401  tgifscgr  25403  iscgrglt  25409  tgbtwnconn1lem3  25469  tgbtwnconn1  25470  legov  25480  legtrd  25484  legtri3  25485  ltgseg  25491  legso  25494  tglinethru  25531  tglnpt2  25536  colline  25544  miriso  25565  midexlem  25587  perpneq  25609  isperp2  25610  footex  25613  midex  25629  opphllem3  25641  opphl  25646  hlpasch  25648  lnopp2hpgb  25655  lmieu  25676  trgcopyeu  25698  dfcgra2  25721  f1otrg  25751  axcontlem2  25845  2pthon3v  26839  clwlksfclwwlk  26962  fsumiunle  29575  2sqmo  29649  ressprs  29655  omndmul2  29712  isarchi3  29741  isarchiofld  29817  fimaproj  29900  txomap  29901  qtophaus  29903  pstmxmet  29940  sqsscirc1  29954  lmxrge0  29998  esumcst  30125  esumfsup  30132  esum2dlem  30154  esum2d  30155  esumiun  30156  ldsysgenld  30223  sigapildsys  30225  omssubadd  30362  signstfvneq0  30649  actfunsnf1o  30682  afsval  30749  noetalem3  31865  nn0prpwlem  32317  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  mblfinlem3  33448  itg2addnclem  33461  sstotbnd2  33573  prdstotbnd  33593  lcfl8  36791  diophren  37377  rencldnfilem  37384  pellex  37399  pell1234qrdich  37425  pell1qrgap  37438  pellfundex  37450  iunconnlem2  39171  suplesup  39555  infleinflem2  39587  xrralrecnnle  39602  rexabslelem  39645  limcrecl  39861  limcleqr  39876  0ellimcdiv  39881  limclner  39883  limsupubuz  39945  limsupvaluz2  39970  supcnvlimsup  39972  climxrre  39982  xlimmnfvlem2  40059  xlimmnfv  40060  xlimpnfvlem2  40063  xlimpnfv  40064  icccncfext  40100  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  fourierdlem50  40373  fourierdlem51  40374  fourierdlem80  40403  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  omef  40710  smflimlem2  40980  smflimlem4  40982  smfmullem3  41000  reuccatpfxs1  41434