Theorem simp1r 968

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 108	. 2 |- ( ( ph /\ ps ) -> ps )
2	1	3ad2ant1 964	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  simpl1r  995  simpr1r  1001  simp11r  1055  simp21r  1061  simp31r  1067  vtoclgft  2669  en2lp  4370  funprg  5064  nnsucsssuc  6253  ecopovtrn  6389  ecopovtrng  6392  addassnqg  6941  distrnqg  6946  ltsonq  6957  ltanqg  6959  ltmnqg  6960  distrnq0  7018  addassnq0  7021  prarloclem5  7059  recexprlem1ssl  7192  recexprlem1ssu  7193  mulasssrg  7304  distrsrg  7305  lttrsr  7308  ltsosr  7310  ltasrg  7316  mulextsr1lem  7325  mulextsr1  7326  axmulass  7408  axdistr  7409  dmdcanap  8189  lt2msq1  8346  lediv2  8352  modqdi  9799  expaddzaplem  9998  expaddzap  9999  expmulzap  10001  prmexpb  11408