Theorem simp1r 1049

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1r	|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )

Proof of Theorem simp1r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	3ad2ant1 1045	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simpl1r  1076  simpr1r  1082  simp11r  1136  simp21r  1142  simp31r  1148  vtoclgft  2865  en2lp  4676  funprg  5406  nnsucsssuc  6725  ecopovtrn  6866  ecopovtrng  6869  addassnqg  7697  distrnqg  7702  ltsonq  7713  ltanqg  7715  ltmnqg  7716  distrnq0  7774  addassnq0  7777  prarloclem5  7815  recexprlem1ssl  7948  recexprlem1ssu  7949  mulasssrg  8073  distrsrg  8074  lttrsr  8077  ltsosr  8079  ltasrg  8085  mulextsr1lem  8095  mulextsr1  8096  axmulass  8188  axdistr  8189  dmdcanap  8996  lt2msq1  9159  lediv2  9165  xaddass2  10203  xlt2add  10213  modqdi  10754  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  swrdspsleq  11359  pfxeq  11388  bdtrilem  11924  xrbdtri  11961  bitsfzo  12641  prmexpb  12848  4sqlem18  13106  mgmsscl  13574  subgabl  14049  cnptoprest  15104  ssblps  15290  ssbl  15291  rplogbchbase  15815  rplogbreexp  15818  relogbcxpbap  15830  lgssq  15913  uhgr2edg  16201