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  2788  en2lp  4554  funprg  5267  nnsucsssuc  6493  ecopovtrn  6632  ecopovtrng  6635  addassnqg  7381  distrnqg  7386  ltsonq  7397  ltanqg  7399  ltmnqg  7400  distrnq0  7458  addassnq0  7461  prarloclem5  7499  recexprlem1ssl  7632  recexprlem1ssu  7633  mulasssrg  7757  distrsrg  7758  lttrsr  7761  ltsosr  7763  ltasrg  7769  mulextsr1lem  7779  mulextsr1  7780  axmulass  7872  axdistr  7873  dmdcanap  8679  lt2msq1  8842  lediv2  8848  xaddass2  9870  xlt2add  9880  modqdi  10392  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  bdtrilem  11247  xrbdtri  11284  prmexpb  12151  mgmsscl  12780  cnptoprest  13742  ssblps  13928  ssbl  13929  rplogbchbase  14371  rplogbreexp  14374  relogbcxpbap  14386  lgssq  14444