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  7072  finexdc  7073  dcfi  7159  difinfsn  7278  nnnninfeq2  7307  nninfisol  7311  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  suplocexprlemru  7917  suplocsrlemb  8004  suplocsrlem  8006  aptap  8808  supinfneg  9802  infsupneg  9803  xaddf  10052  xaddval  10053  nn0ltexp2  10943  hashunlem  11038  swrdccatin1  11272  reuccatpfxs1  11294  xrmaxiflemcl  11771  xrmaxiflemlub  11774  xrmaxltsup  11784  sumeq2  11885  fsumconst  11980  prodeq2  12083  fprodconst  12146  nninfctlemfo  12576  prdsval  13321  sgrpidmndm  13468  mhmmnd  13668  ghmcmn  13879  issrg  13943  cncnp  14919  neitx  14957  dedekindeulemlu  15310  suplociccreex  15313  dedekindicclemlu  15319  cnplimclemr  15358  limccnp2cntop  15366  logbgcd1irrap  15659  lgsval  15698  pw1ndom3  16413