Theorem simp1r 1006

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 109	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	3ad2ant1 1002	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpl1r  1033  simpr1r  1039  simp11r  1093  simp21r  1099  simp31r  1105  vtoclgft  2731  en2lp  4464  funprg  5168  nnsucsssuc  6381  ecopovtrn  6519  ecopovtrng  6522  addassnqg  7183  distrnqg  7188  ltsonq  7199  ltanqg  7201  ltmnqg  7202  distrnq0  7260  addassnq0  7263  prarloclem5  7301  recexprlem1ssl  7434  recexprlem1ssu  7435  mulasssrg  7559  distrsrg  7560  lttrsr  7563  ltsosr  7565  ltasrg  7571  mulextsr1lem  7581  mulextsr1  7582  axmulass  7674  axdistr  7675  dmdcanap  8475  lt2msq1  8636  lediv2  8642  xaddass2  9646  xlt2add  9656  modqdi  10158  expaddzaplem  10329  expaddzap  10330  expmulzap  10332  bdtrilem  11003  xrbdtri  11038  prmexpb  11818  cnptoprest  12397  ssblps  12583  ssbl  12584