Theorem simplr2 1071

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 1035	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ps )
2	1	adantr 276	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  prarloclemlt  7860  prarloclemlo  7861  seq3f1oleml  10953  ccatswrd  11442  resqrexlemdecn  11778  pcdvdstr  13106  ennnfoneleminc  13302  grprcan  13842  mulgnn0dir  13955  prdssgrpd  14191  prdsmndd  14194  lmodprop2d  14685  lssintclm  14721  psrbaglesuppg  15057  restopnb  15282  cnptopresti  15339  blsscls2  15594