Theorem simplr3 1044

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

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

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 983

This theorem is referenced by:  netap  7386  prarloclemlt  7626  prarloclemlo  7627  ccatswrd  11146  resqrexlemdecn  11398  summodclem2  11768  isumss2  11779  pcdvdstr  12725  ennnfoneleminc  12857  prdssgrpd  13322  prdsmndd  13355  grprcan  13444  mulgnn0dir  13563  mulgdir  13565  mulgass  13570  lmodprop2d  14185  lssintclm  14221  psrbaglesuppg  14509  restopnb  14728  blsscls2  15040