Theorem simp1r 963

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

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

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 921

This theorem is referenced by:  simpl1r  990  simpr1r  996  simp11r  1050  simp21r  1056  simp31r  1062  vtoclgft  2649  en2lp  4297  funprg  4969  nnsucsssuc  6094  ecopovtrn  6226  ecopovtrng  6229  addassnqg  6572  distrnqg  6577  ltsonq  6588  ltanqg  6590  ltmnqg  6591  distrnq0  6649  addassnq0  6652  prarloclem5  6690  recexprlem1ssl  6823  recexprlem1ssu  6824  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltsosr  6941  ltasrg  6947  mulextsr1lem  6956  mulextsr1  6957  axmulass  7039  axdistr  7040  dmdcanap  7810  lt2msq1  7963  lediv2  7969  modqdi  9394  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  prmexpb  10530