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  7210  finexdc  7211  fissfi  7267  dcfi  7320  difinfsn  7446  nnnninfeq2  7475  nninfisol  7479  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  suplocexprlemru  8092  suplocsrlemb  8179  suplocsrlem  8181  aptap  8986  supinfneg  10011  infsupneg  10012  xaddf  10263  xaddval  10264  nn0ltexp2  11169  hashunlem  11266  swrdccatin1  11519  reuccatpfxs1  11541  xrmaxiflemcl  12036  xrmaxiflemlub  12039  xrmaxltsup  12049  sumeq2  12150  fsumconst  12246  prodeq2  12349  fprodconst  12412  nninfctlemfo  12842  sgrpidmndm  13792  mhmmnd  13978  ghmcmn  14221  prdsval  14280  issrg  14376  psrbaglefifi  15172  cncnp  15456  neitx  15494  dedekindeulemlu  15847  suplociccreex  15850  dedekindicclemlu  15856  cnplimclemr  15895  limccnp2cntop  15903  logbgcd1irrap  16206  lgsval  16328  usgr1vr  16694  pw1ndom3  17225