Theorem simp-4r 542

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 534	. 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  544  fimax2gtri  7084  finexdc  7085  dcfi  7171  difinfsn  7290  nnnninfeq2  7319  nninfisol  7323  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  suplocexprlemru  7929  suplocsrlemb  8016  suplocsrlem  8018  aptap  8820  supinfneg  9819  infsupneg  9820  xaddf  10069  xaddval  10070  nn0ltexp2  10961  hashunlem  11057  swrdccatin1  11296  reuccatpfxs1  11318  xrmaxiflemcl  11796  xrmaxiflemlub  11799  xrmaxltsup  11809  sumeq2  11910  fsumconst  12005  prodeq2  12108  fprodconst  12171  nninfctlemfo  12601  prdsval  13346  sgrpidmndm  13493  mhmmnd  13693  ghmcmn  13904  issrg  13968  cncnp  14944  neitx  14982  dedekindeulemlu  15335  suplociccreex  15338  dedekindicclemlu  15344  cnplimclemr  15383  limccnp2cntop  15391  logbgcd1irrap  15684  lgsval  15723  usgr1vr  16087  pw1ndom3  16525