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  7641  prarloclemlo  7642  seq3f1oleml  10698  ccatswrd  11161  resqrexlemdecn  11438  pcdvdstr  12765  ennnfoneleminc  12897  prdssgrpd  13362  prdsmndd  13395  grprcan  13484  mulgnn0dir  13603  lmodprop2d  14225  lssintclm  14261  psrbaglesuppg  14549  restopnb  14768  cnptopresti  14825  blsscls2  15080