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  6843  finexdc  6844  difinfsn  7038  nnnninfeq2  7066  nninfisol  7070  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  suplocexprlemru  7633  suplocsrlemb  7720  suplocsrlem  7722  supinfneg  9500  infsupneg  9501  xaddf  9741  xaddval  9742  hashunlem  10671  xrmaxiflemcl  11135  xrmaxiflemlub  11138  xrmaxltsup  11148  sumeq2  11249  fsumconst  11344  prodeq2  11447  fprodconst  11510  cncnp  12601  neitx  12639  dedekindeulemlu  12970  suplociccreex  12973  dedekindicclemlu  12979  cnplimclemr  13009  limccnp2cntop  13017  logbgcd1irrap  13258