Theorem simp1r 1049

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

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

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 1007

This theorem is referenced by:  simpl1r  1076  simpr1r  1082  simp11r  1136  simp21r  1142  simp31r  1148  vtoclgft  2855  en2lp  4658  funprg  5387  nnsucsssuc  6703  ecopovtrn  6844  ecopovtrng  6847  addassnqg  7645  distrnqg  7650  ltsonq  7661  ltanqg  7663  ltmnqg  7664  distrnq0  7722  addassnq0  7725  prarloclem5  7763  recexprlem1ssl  7896  recexprlem1ssu  7897  mulasssrg  8021  distrsrg  8022  lttrsr  8025  ltsosr  8027  ltasrg  8033  mulextsr1lem  8043  mulextsr1  8044  axmulass  8136  axdistr  8137  dmdcanap  8944  lt2msq1  9107  lediv2  9113  xaddass2  10149  xlt2add  10159  modqdi  10700  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  swrdspsleq  11297  pfxeq  11326  bdtrilem  11862  xrbdtri  11899  bitsfzo  12579  prmexpb  12786  4sqlem18  13044  mgmsscl  13507  subgabl  13982  cnptoprest  15033  ssblps  15219  ssbl  15220  rplogbchbase  15744  rplogbreexp  15747  relogbcxpbap  15759  lgssq  15842  uhgr2edg  16130