Theorem simp1r 1024

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

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

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 982

This theorem is referenced by:  simpl1r  1051  simpr1r  1057  simp11r  1111  simp21r  1117  simp31r  1123  vtoclgft  2811  en2lp  4587  funprg  5305  nnsucsssuc  6547  ecopovtrn  6688  ecopovtrng  6691  addassnqg  7444  distrnqg  7449  ltsonq  7460  ltanqg  7462  ltmnqg  7463  distrnq0  7521  addassnq0  7524  prarloclem5  7562  recexprlem1ssl  7695  recexprlem1ssu  7696  mulasssrg  7820  distrsrg  7821  lttrsr  7824  ltsosr  7826  ltasrg  7832  mulextsr1lem  7842  mulextsr1  7843  axmulass  7935  axdistr  7936  dmdcanap  8743  lt2msq1  8906  lediv2  8912  xaddass2  9939  xlt2add  9949  modqdi  10466  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  bdtrilem  11385  xrbdtri  11422  prmexpb  12292  4sqlem18  12549  mgmsscl  12947  subgabl  13405  cnptoprest  14418  ssblps  14604  ssbl  14605  rplogbchbase  15123  rplogbreexp  15126  relogbcxpbap  15138  lgssq  15197