Theorem simp-4r 548

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 540	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-5r  550  fimax2gtri  7206  finexdc  7207  fissfi  7263  dcfi  7315  difinfsn  7440  nnnninfeq2  7469  nninfisol  7473  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  suplocexprlemru  8086  suplocsrlemb  8173  suplocsrlem  8175  aptap  8980  supinfneg  10004  infsupneg  10005  xaddf  10256  xaddval  10257  nn0ltexp2  11161  hashunlem  11258  swrdccatin1  11511  reuccatpfxs1  11533  xrmaxiflemcl  12027  xrmaxiflemlub  12030  xrmaxltsup  12040  sumeq2  12141  fsumconst  12237  prodeq2  12340  fprodconst  12403  nninfctlemfo  12833  sgrpidmndm  13782  mhmmnd  13968  ghmcmn  14180  prdsval  14222  issrg  14318  cncnp  15380  neitx  15418  dedekindeulemlu  15771  suplociccreex  15774  dedekindicclemlu  15780  cnplimclemr  15819  limccnp2cntop  15827  logbgcd1irrap  16125  lgsval  16221  usgr1vr  16587  pw1ndom3  17118