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  8678  lt2msq1  8841  lediv2  8847  xaddass2  9869  xlt2add  9879  modqdi  10391  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  bdtrilem  11246  xrbdtri  11283  prmexpb  12150  mgmsscl  12779  cnptoprest  13709  ssblps  13895  ssbl  13896  rplogbchbase  14338  rplogbreexp  14341  relogbcxpbap  14353  lgssq  14411