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  6997  finexdc  6998  dcfi  7082  difinfsn  7201  nnnninfeq2  7230  nninfisol  7234  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  suplocexprlemru  7831  suplocsrlemb  7918  suplocsrlem  7920  aptap  8722  supinfneg  9715  infsupneg  9716  xaddf  9965  xaddval  9966  nn0ltexp2  10852  hashunlem  10947  xrmaxiflemcl  11527  xrmaxiflemlub  11530  xrmaxltsup  11540  sumeq2  11641  fsumconst  11736  prodeq2  11839  fprodconst  11902  nninfctlemfo  12332  prdsval  13076  sgrpidmndm  13223  mhmmnd  13423  ghmcmn  13634  issrg  13698  cncnp  14673  neitx  14711  dedekindeulemlu  15064  suplociccreex  15067  dedekindicclemlu  15073  cnplimclemr  15112  limccnp2cntop  15120  logbgcd1irrap  15413  lgsval  15452