Theorem simp-4r 532

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 524	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
2	1	adantr 274	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-5r  534  fimax2gtri  6863  finexdc  6864  dcfi  6942  difinfsn  7061  nnnninfeq2  7089  nninfisol  7093  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  suplocexprlemru  7656  suplocsrlemb  7743  suplocsrlem  7745  supinfneg  9529  infsupneg  9530  xaddf  9776  xaddval  9777  nn0ltexp2  10619  hashunlem  10713  xrmaxiflemcl  11182  xrmaxiflemlub  11185  xrmaxltsup  11195  sumeq2  11296  fsumconst  11391  prodeq2  11494  fprodconst  11557  cncnp  12830  neitx  12868  dedekindeulemlu  13199  suplociccreex  13202  dedekindicclemlu  13208  cnplimclemr  13238  limccnp2cntop  13246  logbgcd1irrap  13488  lgsval  13505