Theorem simp1r 1053

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

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

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 1011

This theorem is referenced by:  simpl1r  1080  simpr1r  1086  simp11r  1140  simp21r  1146  simp31r  1152  vtoclgft  2873  en2lp  4696  funprg  5426  nnsucsssuc  6755  ecopovtrn  6896  ecopovtrng  6899  addassnqg  7739  distrnqg  7744  ltsonq  7755  ltanqg  7757  ltmnqg  7758  distrnq0  7816  addassnq0  7819  prarloclem5  7857  recexprlem1ssl  7990  recexprlem1ssu  7991  mulasssrg  8115  distrsrg  8116  lttrsr  8119  ltsosr  8121  ltasrg  8127  mulextsr1lem  8137  mulextsr1  8138  axmulass  8230  axdistr  8231  dmdcanap  9042  lt2msq1  9205  lediv2  9211  xaddass2  10251  xlt2add  10261  modqdi  10807  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  swrdspsleq  11417  pfxeq  11446  bdtrilem  11983  xrbdtri  12020  bitsfzo  12700  prmexpb  12907  4sqlem18  13165  mgmsscl  13658  subgabl  14113  rng1zrlem  14233  cnptoprest  15263  ssblps  15449  ssbl  15450  rplogbchbase  15975  rplogbreexp  15978  relogbcxpbap  15990  lgssq  16073  uhgr2edg  16361