Theorem simp1r 1012

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 1008	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )

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

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 970

This theorem is referenced by:  simpl1r  1039  simpr1r  1045  simp11r  1099  simp21r  1105  simp31r  1111  vtoclgft  2776  en2lp  4531  funprg  5238  nnsucsssuc  6460  ecopovtrn  6598  ecopovtrng  6601  addassnqg  7323  distrnqg  7328  ltsonq  7339  ltanqg  7341  ltmnqg  7342  distrnq0  7400  addassnq0  7403  prarloclem5  7441  recexprlem1ssl  7574  recexprlem1ssu  7575  mulasssrg  7699  distrsrg  7700  lttrsr  7703  ltsosr  7705  ltasrg  7711  mulextsr1lem  7721  mulextsr1  7722  axmulass  7814  axdistr  7815  dmdcanap  8618  lt2msq1  8780  lediv2  8786  xaddass2  9806  xlt2add  9816  modqdi  10327  expaddzaplem  10498  expaddzap  10499  expmulzap  10501  bdtrilem  11180  xrbdtri  11217  prmexpb  12083  mgmsscl  12592  cnptoprest  12879  ssblps  13065  ssbl  13066  rplogbchbase  13508  rplogbreexp  13511  relogbcxpbap  13523  lgssq  13581