Theorem simp-4r 544

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp-5r  546  fimax2gtri  7134  finexdc  7135  dcfi  7223  difinfsn  7342  nnnninfeq2  7371  nninfisol  7375  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  suplocexprlemru  7982  suplocsrlemb  8069  suplocsrlem  8071  aptap  8872  supinfneg  9873  infsupneg  9874  xaddf  10123  xaddval  10124  nn0ltexp2  11017  hashunlem  11113  swrdccatin1  11355  reuccatpfxs1  11377  xrmaxiflemcl  11868  xrmaxiflemlub  11871  xrmaxltsup  11881  sumeq2  11982  fsumconst  12078  prodeq2  12181  fprodconst  12244  nninfctlemfo  12674  prdsval  13419  sgrpidmndm  13566  mhmmnd  13766  ghmcmn  13977  issrg  14042  cncnp  15024  neitx  15062  dedekindeulemlu  15415  suplociccreex  15418  dedekindicclemlu  15424  cnplimclemr  15463  limccnp2cntop  15471  logbgcd1irrap  15764  lgsval  15806  usgr1vr  16172  pw1ndom3  16693