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  6957  finexdc  6958  dcfi  7040  difinfsn  7159  nnnninfeq2  7188  nninfisol  7192  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  suplocexprlemru  7779  suplocsrlemb  7866  suplocsrlem  7868  aptap  8669  supinfneg  9660  infsupneg  9661  xaddf  9910  xaddval  9911  nn0ltexp2  10780  hashunlem  10875  xrmaxiflemcl  11388  xrmaxiflemlub  11391  xrmaxltsup  11401  sumeq2  11502  fsumconst  11597  prodeq2  11700  fprodconst  11763  nninfctlemfo  12177  sgrpidmndm  13001  mhmmnd  13186  ghmcmn  13397  issrg  13461  cncnp  14398  neitx  14436  dedekindeulemlu  14775  suplociccreex  14778  dedekindicclemlu  14784  cnplimclemr  14823  limccnp2cntop  14831  logbgcd1irrap  15102  lgsval  15120