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  7059  finexdc  7060  dcfi  7144  difinfsn  7263  nnnninfeq2  7292  nninfisol  7296  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  suplocexprlemru  7902  suplocsrlemb  7989  suplocsrlem  7991  aptap  8793  supinfneg  9786  infsupneg  9787  xaddf  10036  xaddval  10037  nn0ltexp2  10926  hashunlem  11021  swrdccatin1  11252  reuccatpfxs1  11274  xrmaxiflemcl  11751  xrmaxiflemlub  11754  xrmaxltsup  11764  sumeq2  11865  fsumconst  11960  prodeq2  12063  fprodconst  12126  nninfctlemfo  12556  prdsval  13301  sgrpidmndm  13448  mhmmnd  13648  ghmcmn  13859  issrg  13923  cncnp  14898  neitx  14936  dedekindeulemlu  15289  suplociccreex  15292  dedekindicclemlu  15298  cnplimclemr  15337  limccnp2cntop  15345  logbgcd1irrap  15638  lgsval  15677