Theorem simplr3 1068

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

Assertion

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

Proof of Theorem simplr3

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

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

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 1007

This theorem is referenced by:  netap  7584  prarloclemlt  7824  prarloclemlo  7825  ccatswrd  11387  pfxccat3  11451  resqrexlemdecn  11722  summodclem2  12093  isumss2  12104  pcdvdstr  13050  ennnfoneleminc  13246  grprcan  13792  mulgnn0dir  13905  mulgdir  13907  mulgass  13912  prdssgrpd  14133  prdsmndd  14136  lmodprop2d  14622  lssintclm  14658  psrbaglesuppg  14947  restopnb  15172  blsscls2  15484