Theorem simp1r 1007

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  simpl1r  1034  simpr1r  1040  simp11r  1094  simp21r  1100  simp31r  1106  vtoclgft  2762  en2lp  4513  funprg  5220  nnsucsssuc  6439  ecopovtrn  6577  ecopovtrng  6580  addassnqg  7302  distrnqg  7307  ltsonq  7318  ltanqg  7320  ltmnqg  7321  distrnq0  7379  addassnq0  7382  prarloclem5  7420  recexprlem1ssl  7553  recexprlem1ssu  7554  mulasssrg  7678  distrsrg  7679  lttrsr  7682  ltsosr  7684  ltasrg  7690  mulextsr1lem  7700  mulextsr1  7701  axmulass  7793  axdistr  7794  dmdcanap  8595  lt2msq1  8756  lediv2  8762  xaddass2  9774  xlt2add  9784  modqdi  10291  expaddzaplem  10462  expaddzap  10463  expmulzap  10465  bdtrilem  11138  xrbdtri  11173  prmexpb  12026  cnptoprest  12650  ssblps  12836  ssbl  12837  rplogbchbase  13278  rplogbreexp  13281  relogbcxpbap  13293