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  6959  finexdc  6960  dcfi  7042  difinfsn  7161  nnnninfeq2  7190  nninfisol  7194  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  suplocexprlemru  7781  suplocsrlemb  7868  suplocsrlem  7870  aptap  8671  supinfneg  9663  infsupneg  9664  xaddf  9913  xaddval  9914  nn0ltexp2  10783  hashunlem  10878  xrmaxiflemcl  11391  xrmaxiflemlub  11394  xrmaxltsup  11404  sumeq2  11505  fsumconst  11600  prodeq2  11703  fprodconst  11766  nninfctlemfo  12180  sgrpidmndm  13004  mhmmnd  13189  ghmcmn  13400  issrg  13464  cncnp  14409  neitx  14447  dedekindeulemlu  14800  suplociccreex  14803  dedekindicclemlu  14809  cnplimclemr  14848  limccnp2cntop  14856  logbgcd1irrap  15143  lgsval  15161