Theorem simp2rr 1078

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

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 985

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 189  df-an 373  df-3an 987

This theorem is referenced by:  tfrlem5  7098  omeu  7286  gruina  9243  4sqlem18OLD  14906  4sqlem18  14912  vdwlem10  14940  mdetuni0  19646  mdetmul  19648  tsmsxp  21169  ax5seglem3  24961  btwnconn1lem1  30854  btwnconn1lem3  30856  btwnconn1lem4  30857  btwnconn1lem5  30858  btwnconn1lem6  30859  btwnconn1lem7  30860  btwnconn1lem12  30865  linethru  30920  2llnjN  33132  2lplnja  33184  2lplnj  33185  cdlemblem  33358  dalaw  33451  pclfinN  33465  lhpmcvr4N  33591  cdlemb2  33606  cdleme01N  33787  cdleme0ex2N  33790  cdleme7c  33811  cdlemefrs29bpre0  33963  cdlemefrs29cpre1  33965  cdlemefrs32fva1  33968  cdlemefs32sn1aw  33981  cdleme41sn3a  34000  cdleme48fv  34066  cdlemk21-2N  34458  dihmeetlem13N  34887  pellex  35679  lmhmfgsplit  35944  iunrelexpmin1  36300