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  7049  injresinj  11975  reuccats1  12783  prdsval  15296  catcocl  15534  catass  15535  catpropd  15557  cidpropd  15558  monpropd  15585  subccocl  15693  funcco  15719  funcpropd  15748  fucpropd  15825  initoeu2lem1  15852  xpcpropd  16036  curf2ndf  16075  drsdirfi  16126  mhmmnd  16751  gsmsymgreqlem2  17015  dfod2  17158  ghmcmn  17415  psgndif  19112  dmatscmcl  19470  smatvscl  19491  cpmatmcllem  19684  pm2mpmhmlem2  19785  chfacfscmulgsum  19826  chfacfpmmulgsum  19830  neitr  20138  1stcrest  20410  dissnref  20485  dissnlocfin  20486  neitx  20564  tgqtop  20669  ptcmplem3  21011  trust  21186  utoptop  21191  restutopopn  21195  ustuqtop2  21199  ustuqtop4  21201  utop3cls  21208  isucn2  21236  met1stc  21478  prdsxmslem2  21486  metustexhalf  21513  cfilucfil  21516  metucn  21528  aannenlem1  23226  ulmuni  23289  lgamucov  23905  pntpbnd  24368  pntlem3  24389  istrkgb  24445  tgbtwndiff  24492  tgifscgr  24495  iscgrglt  24501  tgbtwnconn1lem3  24561  tgbtwnconn1  24562  legov  24572  legtrd  24576  legtri3  24577  ltgseg  24583  legso  24586  tglinethru  24623  tglnpt2  24628  colline  24636  miriso  24657  midexlem  24679  perpneq  24701  isperp2  24702  footex  24705  midex  24721  opphllem3  24733  opphl  24738  hlpasch  24740  lnopp2hpgb  24747  lmieu  24768  trgcopyeu  24790  dfcgra2  24813  f1otrg  24843  axcontlem2  24937  pthdepisspth  25246  usgra2adedgwlkonALT  25286  clwlkfclwwlk  25514  2sqmo  28361  ressprs  28367  omndmul2  28426  isarchi3  28455  isarchiofld  28532  fimaproj  28612  txomap  28613  qtophaus  28615  pstmxmet  28652  sqsscirc1  28666  lmxrge0  28710  esumcst  28836  esumfsup  28843  esum2dlem  28865  esum2d  28866  esumiun  28867  ldsysgenld  28934  sigapildsys  28936  omssubadd  29080  omssubaddOLD  29084  signstfvneq0  29413  afsval  29440  nn0prpwlem  30927  mblfinlem3  31886  itg2addnclem  31900  sstotbnd2  32013  prdstotbnd  32033  lcfl8  34982  diophren  35568  rencldnfilem  35575  pellex  35592  pell1234qrdich  35620  pell1qrgap  35633  pellfundex  35647  iunconlem2  37248  suplesup  37459  limcrecl  37592  limcleqr  37608  0ellimcdiv  37613  limclner  37615  icccncfext  37648  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  fourierdlem50  37903  fourierdlem51  37904  fourierdlem80  37933  fourierdlem87  37940  fourierdlem103  37956  fourierdlem104  37957  omef  38168  reuccatpfxs1  38788