Theorem simp1r 1024

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

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

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 982

This theorem is referenced by:  simpl1r  1051  simpr1r  1057  simp11r  1111  simp21r  1117  simp31r  1123  vtoclgft  2822  en2lp  4601  funprg  5323  nnsucsssuc  6577  ecopovtrn  6718  ecopovtrng  6721  addassnqg  7494  distrnqg  7499  ltsonq  7510  ltanqg  7512  ltmnqg  7513  distrnq0  7571  addassnq0  7574  prarloclem5  7612  recexprlem1ssl  7745  recexprlem1ssu  7746  mulasssrg  7870  distrsrg  7871  lttrsr  7874  ltsosr  7876  ltasrg  7882  mulextsr1lem  7892  mulextsr1  7893  axmulass  7985  axdistr  7986  dmdcanap  8794  lt2msq1  8957  lediv2  8963  xaddass2  9991  xlt2add  10001  modqdi  10535  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  bdtrilem  11521  xrbdtri  11558  bitsfzo  12237  prmexpb  12444  4sqlem18  12702  mgmsscl  13164  subgabl  13639  cnptoprest  14682  ssblps  14868  ssbl  14869  rplogbchbase  15393  rplogbreexp  15396  relogbcxpbap  15408  lgssq  15488