Theorem simplr3 1041

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

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

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 980

This theorem is referenced by:  netap  7256  prarloclemlt  7495  prarloclemlo  7496  resqrexlemdecn  11024  summodclem2  11393  isumss2  11404  pcdvdstr  12329  ennnfoneleminc  12415  grprcan  12916  mulgnn0dir  13019  mulgdir  13021  mulgass  13026  lmodprop2d  13444  lssintclm  13477  restopnb  13821  blsscls2  14133