Theorem simp1r 1048

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

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

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 1006

This theorem is referenced by:  simpl1r  1075  simpr1r  1081  simp11r  1135  simp21r  1141  simp31r  1147  vtoclgft  2854  en2lp  4652  funprg  5380  nnsucsssuc  6660  ecopovtrn  6801  ecopovtrng  6804  addassnqg  7602  distrnqg  7607  ltsonq  7618  ltanqg  7620  ltmnqg  7621  distrnq0  7679  addassnq0  7682  prarloclem5  7720  recexprlem1ssl  7853  recexprlem1ssu  7854  mulasssrg  7978  distrsrg  7979  lttrsr  7982  ltsosr  7984  ltasrg  7990  mulextsr1lem  8000  mulextsr1  8001  axmulass  8093  axdistr  8094  dmdcanap  8902  lt2msq1  9065  lediv2  9071  xaddass2  10105  xlt2add  10115  modqdi  10655  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  swrdspsleq  11252  pfxeq  11281  bdtrilem  11817  xrbdtri  11854  bitsfzo  12534  prmexpb  12741  4sqlem18  12999  mgmsscl  13462  subgabl  13937  cnptoprest  14982  ssblps  15168  ssbl  15169  rplogbchbase  15693  rplogbreexp  15696  relogbcxpbap  15708  lgssq  15788  uhgr2edg  16076