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  6915  finexdc  6916  dcfi  6994  difinfsn  7113  nnnninfeq2  7141  nninfisol  7145  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  suplocexprlemru  7732  suplocsrlemb  7819  suplocsrlem  7821  aptap  8621  supinfneg  9609  infsupneg  9610  xaddf  9858  xaddval  9859  nn0ltexp2  10703  hashunlem  10798  xrmaxiflemcl  11267  xrmaxiflemlub  11270  xrmaxltsup  11280  sumeq2  11381  fsumconst  11476  prodeq2  11579  fprodconst  11642  sgrpidmndm  12843  mhmmnd  13011  ghmcmn  13163  issrg  13217  cncnp  14026  neitx  14064  dedekindeulemlu  14395  suplociccreex  14398  dedekindicclemlu  14404  cnplimclemr  14434  limccnp2cntop  14442  logbgcd1irrap  14684  lgsval  14701