Theorem simp1r 1017

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

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

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 975

This theorem is referenced by:  simpl1r  1044  simpr1r  1050  simp11r  1104  simp21r  1110  simp31r  1116  vtoclgft  2780  en2lp  4538  funprg  5248  nnsucsssuc  6471  ecopovtrn  6610  ecopovtrng  6613  addassnqg  7344  distrnqg  7349  ltsonq  7360  ltanqg  7362  ltmnqg  7363  distrnq0  7421  addassnq0  7424  prarloclem5  7462  recexprlem1ssl  7595  recexprlem1ssu  7596  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1lem  7742  mulextsr1  7743  axmulass  7835  axdistr  7836  dmdcanap  8639  lt2msq1  8801  lediv2  8807  xaddass2  9827  xlt2add  9837  modqdi  10348  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  bdtrilem  11202  xrbdtri  11239  prmexpb  12105  mgmsscl  12615  cnptoprest  13033  ssblps  13219  ssbl  13220  rplogbchbase  13662  rplogbreexp  13665  relogbcxpbap  13677  lgssq  13735