Theorem simp1r 1046

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

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

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 1004

This theorem is referenced by:  simpl1r  1073  simpr1r  1079  simp11r  1133  simp21r  1139  simp31r  1145  vtoclgft  2852  en2lp  4650  funprg  5377  nnsucsssuc  6655  ecopovtrn  6796  ecopovtrng  6799  addassnqg  7592  distrnqg  7597  ltsonq  7608  ltanqg  7610  ltmnqg  7611  distrnq0  7669  addassnq0  7672  prarloclem5  7710  recexprlem1ssl  7843  recexprlem1ssu  7844  mulasssrg  7968  distrsrg  7969  lttrsr  7972  ltsosr  7974  ltasrg  7980  mulextsr1lem  7990  mulextsr1  7991  axmulass  8083  axdistr  8084  dmdcanap  8892  lt2msq1  9055  lediv2  9061  xaddass2  10095  xlt2add  10105  modqdi  10644  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  swrdspsleq  11238  pfxeq  11267  bdtrilem  11790  xrbdtri  11827  bitsfzo  12506  prmexpb  12713  4sqlem18  12971  mgmsscl  13434  subgabl  13909  cnptoprest  14953  ssblps  15139  ssbl  15140  rplogbchbase  15664  rplogbreexp  15667  relogbcxpbap  15679  lgssq  15759  uhgr2edg  16045