Theorem simplr3 1072

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

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:  netap  7626  prarloclemlt  7866  prarloclemlo  7867  ccatswrd  11464  pfxccat3  11528  resqrexlemdecn  11800  summodclem2  12174  isumss2  12185  pcdvdstr  13135  ennnfoneleminc  13360  grprcan  13901  mulgnn0dir  14014  mulgdir  14016  mulgass  14021  prdssgrpd  14298  prdsmndd  14301  lmodprop2d  14794  lssintclm  14830  psrbaglesuppg  15166  restopnb  15407  blsscls2  15719