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:  funisfsuppdc  7298  netap  7626  prarloclemlt  7866  prarloclemlo  7867  ccatswrd  11463  pfxccat3  11527  resqrexlemdecn  11799  summodclem2  12173  isumss2  12184  pcdvdstr  13134  ennnfoneleminc  13359  grprcan  13900  mulgnn0dir  14013  mulgdir  14015  mulgass  14020  prdssgrpd  14297  prdsmndd  14300  lmodprop2d  14793  lssintclm  14829  psrbaglesuppg  15170  mplsubgfilemcl  15232  restopnb  15424  blsscls2  15736