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  2823  en2lp  4602  funprg  5324  nnsucsssuc  6578  ecopovtrn  6719  ecopovtrng  6722  addassnqg  7495  distrnqg  7500  ltsonq  7511  ltanqg  7513  ltmnqg  7514  distrnq0  7572  addassnq0  7575  prarloclem5  7613  recexprlem1ssl  7746  recexprlem1ssu  7747  mulasssrg  7871  distrsrg  7872  lttrsr  7875  ltsosr  7877  ltasrg  7883  mulextsr1lem  7893  mulextsr1  7894  axmulass  7986  axdistr  7987  dmdcanap  8795  lt2msq1  8958  lediv2  8964  xaddass2  9992  xlt2add  10002  modqdi  10537  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  swrdspsleq  11120  bdtrilem  11550  xrbdtri  11587  bitsfzo  12266  prmexpb  12473  4sqlem18  12731  mgmsscl  13193  subgabl  13668  cnptoprest  14711  ssblps  14897  ssbl  14898  rplogbchbase  15422  rplogbreexp  15425  relogbcxpbap  15437  lgssq  15517