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  7024  finexdc  7025  dcfi  7109  difinfsn  7228  nnnninfeq2  7257  nninfisol  7261  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  suplocexprlemru  7867  suplocsrlemb  7954  suplocsrlem  7956  aptap  8758  supinfneg  9751  infsupneg  9752  xaddf  10001  xaddval  10002  nn0ltexp2  10891  hashunlem  10986  swrdccatin1  11216  reuccatpfxs1  11238  xrmaxiflemcl  11671  xrmaxiflemlub  11674  xrmaxltsup  11684  sumeq2  11785  fsumconst  11880  prodeq2  11983  fprodconst  12046  nninfctlemfo  12476  prdsval  13220  sgrpidmndm  13367  mhmmnd  13567  ghmcmn  13778  issrg  13842  cncnp  14817  neitx  14855  dedekindeulemlu  15208  suplociccreex  15211  dedekindicclemlu  15217  cnplimclemr  15256  limccnp2cntop  15264  logbgcd1irrap  15557  lgsval  15596