Theorem simpll3 1064

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll3	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simpl3 1028	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )

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

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 1006

This theorem is referenced by:  frirrg  4447  fidceq  7055  fidifsnen  7056  en2eqpr  7098  iunfidisj  7144  ordiso2  7233  addlocpr  7755  aptiprlemu  7859  xltadd1  10110  xlesubadd  10117  icoshftf1o  10225  fztri3or  10273  elfzonelfzo  10474  exp3val  10802  nn0ltexp2  10970  hashun  11067  swrdclg  11230  subcn2  11871  divalglemeuneg  12483  dvdslegcd  12534  lcmledvds  12641  rpdvds  12670  cncongr2  12675  qexpz  12924  iuncld  14838  iscnp4  14941  cnpnei  14942  cnconst2  14956  cnpdis  14965  txcn  14998  blssps  15150  blss  15151  metcnp3  15234  metcnp  15235  lgsfcl2  15734  lgsdir  15763  lgsne0  15766