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  2814  en2lp  4591  funprg  5309  nnsucsssuc  6559  ecopovtrn  6700  ecopovtrng  6703  addassnqg  7466  distrnqg  7471  ltsonq  7482  ltanqg  7484  ltmnqg  7485  distrnq0  7543  addassnq0  7546  prarloclem5  7584  recexprlem1ssl  7717  recexprlem1ssu  7718  mulasssrg  7842  distrsrg  7843  lttrsr  7846  ltsosr  7848  ltasrg  7854  mulextsr1lem  7864  mulextsr1  7865  axmulass  7957  axdistr  7958  dmdcanap  8766  lt2msq1  8929  lediv2  8935  xaddass2  9962  xlt2add  9972  modqdi  10501  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  bdtrilem  11421  xrbdtri  11458  bitsfzo  12137  prmexpb  12344  4sqlem18  12602  mgmsscl  13063  subgabl  13538  cnptoprest  14559  ssblps  14745  ssbl  14746  rplogbchbase  15270  rplogbreexp  15273  relogbcxpbap  15285  lgssq  15365