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  7621  prarloclemlt  7861  prarloclemlo  7862  ccatswrd  11458  pfxccat3  11522  resqrexlemdecn  11794  summodclem2  12168  isumss2  12179  pcdvdstr  13129  ennnfoneleminc  13354  grprcan  13895  mulgnn0dir  14008  mulgdir  14010  mulgass  14015  prdssgrpd  14275  prdsmndd  14278  lmodprop2d  14769  lssintclm  14805  psrbaglesuppg  15141  restopnb  15373  blsscls2  15685