Theorem simp2rr 1066

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 757	. 2 |- ( ( ch /\ ( ph /\ ps ) ) -> ps )
2	1	3ad2ant2 1018	1 |- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ps )

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

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 975

This theorem is referenced by:  tfrlem5  7067  omeu  7252  gruina  9213  4sqlem18  14492  vdwlem10  14520  mdetuni0  19250  mdetmul  19252  tsmsxp  20783  ax5seglem3  24361  btwnconn1lem1  29921  btwnconn1lem3  29923  btwnconn1lem4  29924  btwnconn1lem5  29925  btwnconn1lem6  29926  btwnconn1lem7  29927  btwnconn1lem12  29932  linethru  29987  pellex  30954  lmhmfgsplit  31215  2llnjN  35413  2lplnja  35465  2lplnj  35466  cdlemblem  35639  dalaw  35732  pclfinN  35746  lhpmcvr4N  35872  cdlemb2  35887  cdleme01N  36068  cdleme0ex2N  36071  cdleme7c  36092  cdlemefrs29bpre0  36244  cdlemefrs29cpre1  36246  cdlemefrs32fva1  36249  cdlemefs32sn1aw  36262  cdleme41sn3a  36281  cdleme48fv  36347  cdlemk21-2N  36739  dihmeetlem13N  37168