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  7212  finexdc  7213  fissfi  7269  dcfi  7320  difinfsn  7446  nnnninfeq2  7475  nninfisol  7479  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  suplocexprlemru  8092  suplocsrlemb  8179  suplocsrlem  8181  aptap  8986  supinfneg  10010  infsupneg  10011  xaddf  10262  xaddval  10263  nn0ltexp2  11168  hashunlem  11265  swrdccatin1  11518  reuccatpfxs1  11540  xrmaxiflemcl  12035  xrmaxiflemlub  12038  xrmaxltsup  12048  sumeq2  12149  fsumconst  12245  prodeq2  12348  fprodconst  12411  nninfctlemfo  12841  sgrpidmndm  13791  mhmmnd  13977  ghmcmn  14220  prdsval  14279  issrg  14375  psrbaglefifi  15175  cncnp  15473  neitx  15511  dedekindeulemlu  15864  suplociccreex  15867  dedekindicclemlu  15873  cnplimclemr  15912  limccnp2cntop  15920  logbgcd1irrap  16223  lgsval  16345  usgr1vr  16711  pw1ndom3  17242