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  4645  funprg  5370  nnsucsssuc  6636  ecopovtrn  6777  ecopovtrng  6780  addassnqg  7565  distrnqg  7570  ltsonq  7581  ltanqg  7583  ltmnqg  7584  distrnq0  7642  addassnq0  7645  prarloclem5  7683  recexprlem1ssl  7816  recexprlem1ssu  7817  mulasssrg  7941  distrsrg  7942  lttrsr  7945  ltsosr  7947  ltasrg  7953  mulextsr1lem  7963  mulextsr1  7964  axmulass  8056  axdistr  8057  dmdcanap  8865  lt2msq1  9028  lediv2  9034  xaddass2  10062  xlt2add  10072  modqdi  10609  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  swrdspsleq  11194  pfxeq  11223  bdtrilem  11745  xrbdtri  11782  bitsfzo  12461  prmexpb  12668  4sqlem18  12926  mgmsscl  13389  subgabl  13864  cnptoprest  14907  ssblps  15093  ssbl  15094  rplogbchbase  15618  rplogbreexp  15621  relogbcxpbap  15633  lgssq  15713  uhgr2edg  15998