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  7090  finexdc  7091  dcfi  7179  difinfsn  7298  nnnninfeq2  7327  nninfisol  7331  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  suplocexprlemru  7938  suplocsrlemb  8025  suplocsrlem  8027  aptap  8829  supinfneg  9828  infsupneg  9829  xaddf  10078  xaddval  10079  nn0ltexp2  10970  hashunlem  11066  swrdccatin1  11305  reuccatpfxs1  11327  xrmaxiflemcl  11805  xrmaxiflemlub  11808  xrmaxltsup  11818  sumeq2  11919  fsumconst  12014  prodeq2  12117  fprodconst  12180  nninfctlemfo  12610  prdsval  13355  sgrpidmndm  13502  mhmmnd  13702  ghmcmn  13913  issrg  13977  cncnp  14953  neitx  14991  dedekindeulemlu  15344  suplociccreex  15347  dedekindicclemlu  15353  cnplimclemr  15392  limccnp2cntop  15400  logbgcd1irrap  15693  lgsval  15732  usgr1vr  16098  pw1ndom3  16589