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  11660  swrdsymbeq  12362  prdsval  14414  catcocl  14644  catass  14645  catpropd  14669  cidpropd  14670  monpropd  14697  subccocl  14776  funcco  14802  funcpropd  14831  fucpropd  14908  xpcpropd  15039  curf2ndf  15078  drsdirfi  15129  gsmsymgreqlem2  15957  dfod2  16086  psgndif  18054  neitr  18806  1stcrest  19079  neitx  19202  tgqtop  19307  ptcmplem3  19648  trust  19826  utoptop  19831  restutopopn  19835  ustuqtop2  19839  ustuqtop4  19841  utop3cls  19848  isucn2  19876  met1stc  20118  prdsxmslem2  20126  metustexhalfOLD  20160  metustexhalf  20161  cfilucfilOLD  20166  cfilucfil  20167  metucnOLD  20185  metucn  20186  aannenlem1  21816  ulmuni  21879  pntpbnd  22859  pntlem3  22880  istrkgb  22940  tgbtwndiff  22981  tgifscgr  22983  tgbtwnconn1lem3  23028  tgbtwnconn1  23029  legov  23038  legtrd  23042  legtri3  23043  tglinethru  23064  tglnpt2  23068  colline  23074  miriso  23095  midexlem  23108  perpneq  23127  isperp2  23128  footex  23131  f1otrg  23139  axcontlem2  23233  pthdepisspth  23495  ressprs  26138  omndmul2  26197  isarchi3  26226  isarchiofld  26307  pstmxmet  26346  sqsscirc1  26360  lmxrge0  26404  esumcst  26536  esumfsup  26541  signstfvneq0  26995  afsval  27017  lgamucov  27046  mblfinlem3  28456  itg2addnclem  28469  nn0prpwlem  28543  sstotbnd2  28699  prdstotbnd  28719  diophren  29178  rencldnfilem  29185  pellex  29202  pell1234qrdich  29228  pell1qrgap  29241  pellfundex  29253  reuccats1  30287  clwlkfclwwlk  30543  scmatsubcl  30923  cnstpmatmcllem  31070  iunconlem2  31767  lcfl8  35243