Theorem simp2rr 1058

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

Assertion

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

Proof of Theorem simp2rr

Step	Hyp	Ref	Expression
1		simprr 756	. 2 |- ( ( ch /\ ( ph /\ ps ) ) -> ps )
2	1	3ad2ant2 1010	1 |- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965

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 185  df-an 371  df-3an 967

This theorem is referenced by:  tfrlem5  6837  omeu  7022  gruina  8983  4sqlem18  14021  vdwlem10  14049  mdetuni0  18425  mdetmul  18427  tsmsxp  19727  ax5seglem3  23175  btwnconn1lem1  28116  btwnconn1lem3  28118  btwnconn1lem4  28119  btwnconn1lem5  28120  btwnconn1lem6  28121  btwnconn1lem7  28122  btwnconn1lem12  28127  linethru  28182  pellex  29173  lmhmfgsplit  29436  2llnjN  33208  2lplnja  33260  2lplnj  33261  cdlemblem  33434  dalaw  33527  pclfinN  33541  lhpmcvr4N  33667  cdlemb2  33682  cdleme01N  33862  cdleme0ex2N  33865  cdleme7c  33886  cdlemefrs29bpre0  34037  cdlemefrs29cpre1  34039  cdlemefrs32fva1  34042  cdlemefs32sn1aw  34055  cdleme41sn3a  34074  cdleme48fv  34140  cdlemk21-2N  34532  dihmeetlem13N  34961