Theorem simp-4r 775

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 767	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
2	1	adantr 466	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  simp-5r  777  tfrlem1  7102  injresinj  12022  reuccats1  12822  prdsval  15312  catcocl  15542  catass  15543  catpropd  15565  cidpropd  15566  monpropd  15593  subccocl  15701  funcco  15727  funcpropd  15756  fucpropd  15833  initoeu2lem1  15860  xpcpropd  16044  curf2ndf  16083  drsdirfi  16134  mhmmnd  16759  gsmsymgreqlem2  17023  dfod2  17153  ghmcmn  17407  psgndif  19101  dmatscmcl  19459  smatvscl  19480  cpmatmcllem  19673  pm2mpmhmlem2  19774  chfacfscmulgsum  19815  chfacfpmmulgsum  19819  neitr  20127  1stcrest  20399  dissnref  20474  dissnlocfin  20475  neitx  20553  tgqtop  20658  ptcmplem3  21000  trust  21175  utoptop  21180  restutopopn  21184  ustuqtop2  21188  ustuqtop4  21190  utop3cls  21197  isucn2  21225  met1stc  21467  prdsxmslem2  21475  metustexhalf  21502  cfilucfil  21505  metucn  21517  aannenlem1  23149  ulmuni  23212  lgamucov  23828  pntpbnd  24289  pntlem3  24310  istrkgb  24366  tgbtwndiff  24413  tgifscgr  24416  tgbtwnconn1lem3  24479  tgbtwnconn1  24480  legov  24490  legtrd  24494  legtri3  24495  ltgseg  24501  legso  24504  tglinethru  24540  tglnpt2  24545  colline  24554  miriso  24574  midexlem  24594  perpneq  24616  isperp2  24617  footex  24620  midex  24636  opphllem3  24648  opphl  24653  lnopp2hpgb  24661  lmieu  24682  trgcopyeu  24704  dfcgra2  24726  f1otrg  24747  axcontlem2  24841  pthdepisspth  25149  usgra2adedgwlkonALT  25189  clwlkfclwwlk  25417  2sqmo  28248  ressprs  28254  omndmul2  28313  isarchi3  28342  isarchiofld  28419  fimaproj  28499  txomap  28500  qtophaus  28502  pstmxmet  28539  sqsscirc1  28553  lmxrge0  28597  esumcst  28723  esumfsup  28730  esum2dlem  28752  esum2d  28753  esumiun  28754  ldsysgenld  28821  sigapildsys  28823  omssubadd  28961  signstfvneq0  29249  afsval  29276  nn0prpwlem  30763  mblfinlem3  31682  itg2addnclem  31696  sstotbnd2  31809  prdstotbnd  31829  lcfl8  34778  diophren  35364  rencldnfilem  35371  pellex  35388  pell1234qrdich  35414  pell1qrgap  35427  pellfundex  35439  iunconlem2  36971  suplesup  37170  limcrecl  37280  limcleqr  37296  0ellimcdiv  37301  limclner  37303  icccncfext  37336  ioodvbdlimc1lem2  37375  ioodvbdlimc2lem  37377  fourierdlem50  37587  fourierdlem51  37588  fourierdlem80  37617  fourierdlem87  37624  fourierdlem103  37640  fourierdlem104  37641  omef  37825  reuccatpfxs1  38364