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  6903  finexdc  6904  dcfi  6982  difinfsn  7101  nnnninfeq2  7129  nninfisol  7133  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  suplocexprlemru  7720  suplocsrlemb  7807  suplocsrlem  7809  aptap  8609  supinfneg  9597  infsupneg  9598  xaddf  9846  xaddval  9847  nn0ltexp2  10691  hashunlem  10786  xrmaxiflemcl  11255  xrmaxiflemlub  11258  xrmaxltsup  11268  sumeq2  11369  fsumconst  11464  prodeq2  11567  fprodconst  11630  sgrpidmndm  12826  mhmmnd  12985  issrg  13153  cncnp  13815  neitx  13853  dedekindeulemlu  14184  suplociccreex  14187  dedekindicclemlu  14193  cnplimclemr  14223  limccnp2cntop  14231  logbgcd1irrap  14473  lgsval  14490