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  6998  finexdc  6999  dcfi  7083  difinfsn  7202  nnnninfeq2  7231  nninfisol  7235  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  suplocexprlemru  7832  suplocsrlemb  7919  suplocsrlem  7921  aptap  8723  supinfneg  9716  infsupneg  9717  xaddf  9966  xaddval  9967  nn0ltexp2  10854  hashunlem  10949  xrmaxiflemcl  11556  xrmaxiflemlub  11559  xrmaxltsup  11569  sumeq2  11670  fsumconst  11765  prodeq2  11868  fprodconst  11931  nninfctlemfo  12361  prdsval  13105  sgrpidmndm  13252  mhmmnd  13452  ghmcmn  13663  issrg  13727  cncnp  14702  neitx  14740  dedekindeulemlu  15093  suplociccreex  15096  dedekindicclemlu  15102  cnplimclemr  15141  limccnp2cntop  15149  logbgcd1irrap  15442  lgsval  15481