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  7082  finexdc  7083  dcfi  7169  difinfsn  7288  nnnninfeq2  7317  nninfisol  7321  exmidfodomrlemr  7401  exmidfodomrlemrALT  7402  suplocexprlemru  7927  suplocsrlemb  8014  suplocsrlem  8016  aptap  8818  supinfneg  9817  infsupneg  9818  xaddf  10067  xaddval  10068  nn0ltexp2  10959  hashunlem  11054  swrdccatin1  11293  reuccatpfxs1  11315  xrmaxiflemcl  11793  xrmaxiflemlub  11796  xrmaxltsup  11806  sumeq2  11907  fsumconst  12002  prodeq2  12105  fprodconst  12168  nninfctlemfo  12598  prdsval  13343  sgrpidmndm  13490  mhmmnd  13690  ghmcmn  13901  issrg  13965  cncnp  14941  neitx  14979  dedekindeulemlu  15332  suplociccreex  15335  dedekindicclemlu  15341  cnplimclemr  15380  limccnp2cntop  15388  logbgcd1irrap  15681  lgsval  15720  usgr1vr  16083  pw1ndom3  16499