Theorem simp1r 1048

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

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

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 1006

This theorem is referenced by:  simpl1r  1075  simpr1r  1081  simp11r  1135  simp21r  1141  simp31r  1147  vtoclgft  2854  en2lp  4652  funprg  5380  nnsucsssuc  6659  ecopovtrn  6800  ecopovtrng  6803  addassnqg  7601  distrnqg  7606  ltsonq  7617  ltanqg  7619  ltmnqg  7620  distrnq0  7678  addassnq0  7681  prarloclem5  7719  recexprlem1ssl  7852  recexprlem1ssu  7853  mulasssrg  7977  distrsrg  7978  lttrsr  7981  ltsosr  7983  ltasrg  7989  mulextsr1lem  7999  mulextsr1  8000  axmulass  8092  axdistr  8093  dmdcanap  8901  lt2msq1  9064  lediv2  9070  xaddass2  10104  xlt2add  10114  modqdi  10653  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  swrdspsleq  11247  pfxeq  11276  bdtrilem  11799  xrbdtri  11836  bitsfzo  12515  prmexpb  12722  4sqlem18  12980  mgmsscl  13443  subgabl  13918  cnptoprest  14962  ssblps  15148  ssbl  15149  rplogbchbase  15673  rplogbreexp  15676  relogbcxpbap  15688  lgssq  15768  uhgr2edg  16056