Theorem simplr2 1043

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

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

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 983

This theorem is referenced by:  prarloclemlt  7606  prarloclemlo  7607  seq3f1oleml  10661  ccatswrd  11123  resqrexlemdecn  11323  pcdvdstr  12650  ennnfoneleminc  12782  prdssgrpd  13247  prdsmndd  13280  grprcan  13369  mulgnn0dir  13488  lmodprop2d  14110  lssintclm  14146  psrbaglesuppg  14434  restopnb  14653  cnptopresti  14710  blsscls2  14965