Theorem simp2rr 1061

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

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

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 970

This theorem is referenced by:  tfrlem5  7039  omeu  7224  gruina  9185  4sqlem18  14328  vdwlem10  14356  mdetuni0  18883  mdetmul  18885  tsmsxp  20385  ax5seglem3  23903  btwnconn1lem1  29300  btwnconn1lem3  29302  btwnconn1lem4  29303  btwnconn1lem5  29304  btwnconn1lem6  29305  btwnconn1lem7  29306  btwnconn1lem12  29311  linethru  29366  pellex  30362  lmhmfgsplit  30625  2llnjN  34238  2lplnja  34290  2lplnj  34291  cdlemblem  34464  dalaw  34557  pclfinN  34571  lhpmcvr4N  34697  cdlemb2  34712  cdleme01N  34892  cdleme0ex2N  34895  cdleme7c  34916  cdlemefrs29bpre0  35067  cdlemefrs29cpre1  35069  cdlemefrs32fva1  35072  cdlemefs32sn1aw  35085  cdleme41sn3a  35104  cdleme48fv  35170  cdlemk21-2N  35562  dihmeetlem13N  35991