Theorem simp-4r 766

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

Syntax hints:   -> wi 4   /\ wa 369

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

This theorem is referenced by:  simp-5r  768  injresinj  11894  swrdsymbeq  12635  reuccats1  12669  prdsval  14710  catcocl  14940  catass  14941  catpropd  14965  cidpropd  14966  monpropd  14993  subccocl  15072  funcco  15098  funcpropd  15127  fucpropd  15204  xpcpropd  15335  curf2ndf  15374  drsdirfi  15425  gsmsymgreqlem2  16261  dfod2  16392  psgndif  18433  dmatscmcl  18800  smatvscl  18821  cpmatmcllem  19014  pm2mpmhmlem2  19115  chfacfscmulgsum  19156  chfacfpmmulgsum  19160  neitr  19475  1stcrest  19748  neitx  19871  tgqtop  19976  ptcmplem3  20317  trust  20495  utoptop  20500  restutopopn  20504  ustuqtop2  20508  ustuqtop4  20510  utop3cls  20517  isucn2  20545  met1stc  20787  prdsxmslem2  20795  metustexhalfOLD  20829  metustexhalf  20830  cfilucfilOLD  20835  cfilucfil  20836  metucnOLD  20854  metucn  20855  aannenlem1  22486  ulmuni  22549  pntpbnd  23529  pntlem3  23550  istrkgb  23608  tgbtwndiff  23653  tgifscgr  23656  tgbtwnconn1lem3  23716  tgbtwnconn1  23717  legov  23727  legtrd  23731  legtri3  23732  ltgseg  23737  legso  23740  tglinethru  23758  tglnpt2  23762  colline  23771  miriso  23791  midexlem  23805  perpneq  23827  isperp2  23828  footex  23831  mideu  23842  lmieu  23855  f1otrg  23878  axcontlem2  23972  pthdepisspth  24280  usgra2adedgwlkonALT  24320  clwlkfclwwlk  24548  ressprs  27333  omndmul2  27392  isarchi3  27421  isarchiofld  27498  fimaproj  27527  txomap  27528  pstmxmet  27540  sqsscirc1  27554  lmxrge0  27598  qtophaus  27665  esumcst  27739  esumfsup  27744  signstfvneq0  28197  afsval  28219  lgamucov  28248  mblfinlem3  29658  itg2addnclem  29671  nn0prpwlem  29745  sstotbnd2  29901  prdstotbnd  29921  diophren  30379  rencldnfilem  30386  pellex  30403  pell1234qrdich  30429  pell1qrgap  30442  pellfundex  30454  limcrecl  31199  limcleqr  31214  addlimc  31218  0ellimcdiv  31219  limclner  31221  icccncfext  31254  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  fourierdlem50  31485  fourierdlem51  31486  fourierdlem80  31515  fourierdlem87  31522  fourierdlem103  31538  fourierdlem104  31539  iunconlem2  32833  lcfl8  36317