Theorem simpl1r 1113

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl1r	|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ps )

Proof of Theorem simpl1r

Step	Hyp	Ref	Expression
1		simp1r 1086	. 2 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )
2	1	adantr 481	1 |- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  soisores  6577  tfisi  7058  omopth2  7664  swrdsbslen  13448  swrdspsleq  13449  repswswrd  13531  ramub1lem1  15730  efgsfo  18152  lbspss  19082  maducoeval2  20446  madurid  20450  decpmatmullem  20576  mp2pm2mplem4  20614  llyrest  21288  ptbasin  21380  basqtop  21514  ustuqtop1  22045  mulcxp  24431  br8d  29422  isarchi2  29739  archiabllem2c  29749  cvmlift2lem10  31294  5segofs  32113  btwnconn1lem13  32206  2llnjaN  34852  paddasslem12  35117  lhp2lt  35287  lhpexle2lem  35295  lhpmcvr3  35311  lhpat3  35332  trlval3  35474  cdleme17b  35574  cdlemefr27cl  35691  cdlemg11b  35930  tendococl  36060  cdlemj3  36111  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk53b  36244  cdlemk35u  36252  cdlemm10N  36407  dihopelvalcpre  36537  dihord6apre  36545  dihord5b  36548  dihglblem5apreN  36580  dihglblem2N  36583  dihmeetlem6  36598  dihmeetlem18N  36613  dvh3dim2  36737  dvh3dim3N  36738  jm2.25lem1  37565  limcleqr  39876  icccncfext  40100  fourierdlem87  40410  sge0seq  40663  smflimsuplem7  41032