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  7866  prarloclemlo  7867  seq3f1oleml  10973  ccatswrd  11463  resqrexlemdecn  11799  pcdvdstr  13134  ennnfoneleminc  13359  grprcan  13900  mulgnn0dir  14013  prdssgrpd  14297  prdsmndd  14300  lmodprop2d  14793  lssintclm  14829  psrbaglesuppg  15170  mplsubgfilemcl  15232  restopnb  15424  cnptopresti  15481  blsscls2  15736