Theorem simp1r 1025

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

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

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 983

This theorem is referenced by:  simpl1r  1052  simpr1r  1058  simp11r  1112  simp21r  1118  simp31r  1124  vtoclgft  2828  en2lp  4620  funprg  5343  nnsucsssuc  6601  ecopovtrn  6742  ecopovtrng  6745  addassnqg  7530  distrnqg  7535  ltsonq  7546  ltanqg  7548  ltmnqg  7549  distrnq0  7607  addassnq0  7610  prarloclem5  7648  recexprlem1ssl  7781  recexprlem1ssu  7782  mulasssrg  7906  distrsrg  7907  lttrsr  7910  ltsosr  7912  ltasrg  7918  mulextsr1lem  7928  mulextsr1  7929  axmulass  8021  axdistr  8022  dmdcanap  8830  lt2msq1  8993  lediv2  8999  xaddass2  10027  xlt2add  10037  modqdi  10574  expaddzaplem  10764  expaddzap  10765  expmulzap  10767  swrdspsleq  11158  pfxeq  11187  bdtrilem  11665  xrbdtri  11702  bitsfzo  12381  prmexpb  12588  4sqlem18  12846  mgmsscl  13308  subgabl  13783  cnptoprest  14826  ssblps  15012  ssbl  15013  rplogbchbase  15537  rplogbreexp  15540  relogbcxpbap  15552  lgssq  15632