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  7348  prarloclemlt  7588  prarloclemlo  7589  resqrexlemdecn  11242  summodclem2  11612  isumss2  11623  pcdvdstr  12569  ennnfoneleminc  12701  prdssgrpd  13165  prdsmndd  13198  grprcan  13287  mulgnn0dir  13406  mulgdir  13408  mulgass  13413  lmodprop2d  14028  lssintclm  14064  psrbaglesuppg  14352  restopnb  14571  blsscls2  14883