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  8978  supinfneg  9995  infsupneg  9996  xaddf  10246  xaddval  10247  nn0ltexp2  11147  hashunlem  11244  swrdccatin1  11497  reuccatpfxs1  11519  xrmaxiflemcl  12011  xrmaxiflemlub  12014  xrmaxltsup  12024  sumeq2  12125  fsumconst  12221  prodeq2  12324  fprodconst  12387  nninfctlemfo  12817  sgrpidmndm  13733  mhmmnd  13919  ghmcmn  14131  prdsval  14173  issrg  14269  cncnp  15331  neitx  15369  dedekindeulemlu  15722  suplociccreex  15725  dedekindicclemlu  15731  cnplimclemr  15770  limccnp2cntop  15778  logbgcd1irrap  16072  lgsval  16123  usgr1vr  16489  pw1ndom3  17020