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  7091  finexdc  7092  dcfi  7180  difinfsn  7299  nnnninfeq2  7328  nninfisol  7332  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  suplocexprlemru  7939  suplocsrlemb  8026  suplocsrlem  8028  aptap  8830  supinfneg  9829  infsupneg  9830  xaddf  10079  xaddval  10080  nn0ltexp2  10972  hashunlem  11068  swrdccatin1  11310  reuccatpfxs1  11332  xrmaxiflemcl  11823  xrmaxiflemlub  11826  xrmaxltsup  11836  sumeq2  11937  fsumconst  12033  prodeq2  12136  fprodconst  12199  nninfctlemfo  12629  prdsval  13374  sgrpidmndm  13521  mhmmnd  13721  ghmcmn  13932  issrg  13997  cncnp  14973  neitx  15011  dedekindeulemlu  15364  suplociccreex  15367  dedekindicclemlu  15373  cnplimclemr  15412  limccnp2cntop  15420  logbgcd1irrap  15713  lgsval  15752  usgr1vr  16118  pw1ndom3  16640