Theorem simp-4r 782

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  simp-5r  784  tfrlem1  7119  injresinj  12056  reuccats1  12873  prdsval  15401  catcocl  15639  catass  15640  catpropd  15662  cidpropd  15663  monpropd  15690  subccocl  15798  funcco  15824  funcpropd  15853  fucpropd  15930  initoeu2lem1  15957  xpcpropd  16141  curf2ndf  16180  drsdirfi  16231  mhmmnd  16856  gsmsymgreqlem2  17120  dfod2  17263  ghmcmn  17520  psgndif  19218  dmatscmcl  19576  smatvscl  19597  cpmatmcllem  19790  pm2mpmhmlem2  19891  chfacfscmulgsum  19932  chfacfpmmulgsum  19936  neitr  20244  1stcrest  20516  dissnref  20591  dissnlocfin  20592  neitx  20670  tgqtop  20775  ptcmplem3  21117  trust  21292  utoptop  21297  restutopopn  21301  ustuqtop2  21305  ustuqtop4  21307  utop3cls  21314  isucn2  21342  met1stc  21584  prdsxmslem2  21592  metustexhalf  21619  cfilucfil  21622  metucn  21634  aannenlem1  23332  ulmuni  23395  lgamucov  24011  pntpbnd  24474  pntlem3  24495  istrkgb  24551  tgbtwndiff  24598  tgifscgr  24601  iscgrglt  24607  tgbtwnconn1lem3  24667  tgbtwnconn1  24668  legov  24678  legtrd  24682  legtri3  24683  ltgseg  24689  legso  24692  tglinethru  24729  tglnpt2  24734  colline  24742  miriso  24763  midexlem  24785  perpneq  24807  isperp2  24808  footex  24811  midex  24827  opphllem3  24839  opphl  24844  hlpasch  24846  lnopp2hpgb  24853  lmieu  24874  trgcopyeu  24896  dfcgra2  24919  f1otrg  24949  axcontlem2  25043  pthdepisspth  25352  usgra2adedgwlkonALT  25392  clwlkfclwwlk  25620  2sqmo  28458  ressprs  28464  omndmul2  28523  isarchi3  28552  isarchiofld  28628  fimaproj  28708  txomap  28709  qtophaus  28711  pstmxmet  28748  sqsscirc1  28762  lmxrge0  28806  esumcst  28932  esumfsup  28939  esum2dlem  28961  esum2d  28962  esumiun  28963  ldsysgenld  29030  sigapildsys  29032  omssubadd  29176  omssubaddOLD  29180  signstfvneq0  29509  afsval  29536  nn0prpwlem  31026  mblfinlem3  32023  itg2addnclem  32037  sstotbnd2  32150  prdstotbnd  32170  lcfl8  35114  diophren  35700  rencldnfilem  35707  pellex  35723  pell1234qrdich  35751  pell1qrgap  35764  pellfundex  35778  iunconlem2  37371  suplesup  37599  limcrecl  37746  limcleqr  37762  0ellimcdiv  37767  limclner  37769  icccncfext  37802  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  fourierdlem50  38057  fourierdlem51  38058  fourierdlem80  38087  fourierdlem87  38094  fourierdlem103  38110  fourierdlem104  38111  omef  38354  reuccatpfxs1  39014  pthdepissPth  39766  2pthon3v-av  39891