Theorem simplr2 1042

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

Assertion

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

Proof of Theorem simplr2

Step	Hyp	Ref	Expression
1		simpr2 1006	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ps )
2	1	adantr 276	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  prarloclemlt  7605  prarloclemlo  7606  seq3f1oleml  10659  resqrexlemdecn  11294  pcdvdstr  12621  ennnfoneleminc  12753  prdssgrpd  13218  prdsmndd  13251  grprcan  13340  mulgnn0dir  13459  lmodprop2d  14081  lssintclm  14117  psrbaglesuppg  14405  restopnb  14624  cnptopresti  14681  blsscls2  14936