Theorem simp1r 1007

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

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

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 965

This theorem is referenced by:  simpl1r  1034  simpr1r  1040  simp11r  1094  simp21r  1100  simp31r  1106  vtoclgft  2739  en2lp  4477  funprg  5181  nnsucsssuc  6396  ecopovtrn  6534  ecopovtrng  6537  addassnqg  7214  distrnqg  7219  ltsonq  7230  ltanqg  7232  ltmnqg  7233  distrnq0  7291  addassnq0  7294  prarloclem5  7332  recexprlem1ssl  7465  recexprlem1ssu  7466  mulasssrg  7590  distrsrg  7591  lttrsr  7594  ltsosr  7596  ltasrg  7602  mulextsr1lem  7612  mulextsr1  7613  axmulass  7705  axdistr  7706  dmdcanap  8506  lt2msq1  8667  lediv2  8673  xaddass2  9683  xlt2add  9693  modqdi  10196  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  bdtrilem  11042  xrbdtri  11077  prmexpb  11865  cnptoprest  12447  ssblps  12633  ssbl  12634  rplogbchbase  13075  rplogbreexp  13078  relogbcxpbap  13090