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  7441  nnnninfeq2  7470  nninfisol  7474  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  suplocexprlemru  8087  suplocsrlemb  8174  suplocsrlem  8176  aptap  8981  supinfneg  10005  infsupneg  10006  xaddf  10257  xaddval  10258  nn0ltexp2  11163  hashunlem  11260  swrdccatin1  11513  reuccatpfxs1  11535  xrmaxiflemcl  12030  xrmaxiflemlub  12033  xrmaxltsup  12043  sumeq2  12144  fsumconst  12240  prodeq2  12343  fprodconst  12406  nninfctlemfo  12836  sgrpidmndm  13786  mhmmnd  13972  ghmcmn  14215  prdsval  14257  issrg  14353  psrbaglefifi  15147  cncnp  15422  neitx  15460  dedekindeulemlu  15813  suplociccreex  15816  dedekindicclemlu  15822  cnplimclemr  15861  limccnp2cntop  15869  logbgcd1irrap  16167  lgsval  16289  usgr1vr  16655  pw1ndom3  17186