Theorem simp1r 1046

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

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

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 1004

This theorem is referenced by:  simpl1r  1073  simpr1r  1079  simp11r  1133  simp21r  1139  simp31r  1145  vtoclgft  2851  en2lp  4646  funprg  5371  nnsucsssuc  6646  ecopovtrn  6787  ecopovtrng  6790  addassnqg  7580  distrnqg  7585  ltsonq  7596  ltanqg  7598  ltmnqg  7599  distrnq0  7657  addassnq0  7660  prarloclem5  7698  recexprlem1ssl  7831  recexprlem1ssu  7832  mulasssrg  7956  distrsrg  7957  lttrsr  7960  ltsosr  7962  ltasrg  7968  mulextsr1lem  7978  mulextsr1  7979  axmulass  8071  axdistr  8072  dmdcanap  8880  lt2msq1  9043  lediv2  9049  xaddass2  10078  xlt2add  10088  modqdi  10626  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  swrdspsleq  11214  pfxeq  11243  bdtrilem  11765  xrbdtri  11802  bitsfzo  12481  prmexpb  12688  4sqlem18  12946  mgmsscl  13409  subgabl  13884  cnptoprest  14928  ssblps  15114  ssbl  15115  rplogbchbase  15639  rplogbreexp  15642  relogbcxpbap  15654  lgssq  15734  uhgr2edg  16019