Theorem simp1r 1022

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

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

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 980

This theorem is referenced by:  simpl1r  1049  simpr1r  1055  simp11r  1109  simp21r  1115  simp31r  1121  vtoclgft  2787  en2lp  4553  funprg  5266  nnsucsssuc  6492  ecopovtrn  6631  ecopovtrng  6634  addassnqg  7380  distrnqg  7385  ltsonq  7396  ltanqg  7398  ltmnqg  7399  distrnq0  7457  addassnq0  7460  prarloclem5  7498  recexprlem1ssl  7631  recexprlem1ssu  7632  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1lem  7778  mulextsr1  7779  axmulass  7871  axdistr  7872  dmdcanap  8677  lt2msq1  8840  lediv2  8846  xaddass2  9868  xlt2add  9878  modqdi  10389  expaddzaplem  10560  expaddzap  10561  expmulzap  10563  bdtrilem  11242  xrbdtri  11279  prmexpb  12145  mgmsscl  12734  cnptoprest  13632  ssblps  13818  ssbl  13819  rplogbchbase  14261  rplogbreexp  14264  relogbcxpbap  14276  lgssq  14334