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  7172  finexdc  7173  fissfi  7229  dcfi  7281  difinfsn  7404  nnnninfeq2  7433  nninfisol  7437  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  suplocexprlemru  8050  suplocsrlemb  8137  suplocsrlem  8139  aptap  8941  supinfneg  9945  infsupneg  9946  xaddf  10196  xaddval  10197  nn0ltexp2  11096  hashunlem  11193  swrdccatin1  11442  reuccatpfxs1  11464  xrmaxiflemcl  11955  xrmaxiflemlub  11958  xrmaxltsup  11968  sumeq2  12069  fsumconst  12165  prodeq2  12268  fprodconst  12331  nninfctlemfo  12761  sgrpidmndm  13681  mhmmnd  13869  ghmcmn  14080  prdsval  14115  issrg  14208  cncnp  15221  neitx  15259  dedekindeulemlu  15612  suplociccreex  15615  dedekindicclemlu  15621  cnplimclemr  15660  limccnp2cntop  15668  logbgcd1irrap  15961  lgsval  16003  usgr1vr  16369  pw1ndom3  16890