Theorem simplr3 1043

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

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

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 982

This theorem is referenced by:  netap  7321  prarloclemlt  7560  prarloclemlo  7561  resqrexlemdecn  11177  summodclem2  11547  isumss2  11558  pcdvdstr  12496  ennnfoneleminc  12628  grprcan  13169  mulgnn0dir  13282  mulgdir  13284  mulgass  13289  lmodprop2d  13904  lssintclm  13940  psrbaglesuppg  14226  restopnb  14417  blsscls2  14729