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  6971  finexdc  6972  dcfi  7056  difinfsn  7175  nnnninfeq2  7204  nninfisol  7208  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  suplocexprlemru  7803  suplocsrlemb  7890  suplocsrlem  7892  aptap  8694  supinfneg  9686  infsupneg  9687  xaddf  9936  xaddval  9937  nn0ltexp2  10818  hashunlem  10913  xrmaxiflemcl  11427  xrmaxiflemlub  11430  xrmaxltsup  11440  sumeq2  11541  fsumconst  11636  prodeq2  11739  fprodconst  11802  nninfctlemfo  12232  prdsval  12975  sgrpidmndm  13122  mhmmnd  13322  ghmcmn  13533  issrg  13597  cncnp  14550  neitx  14588  dedekindeulemlu  14941  suplociccreex  14944  dedekindicclemlu  14950  cnplimclemr  14989  limccnp2cntop  14997  logbgcd1irrap  15290  lgsval  15329