Theorem simpll3 1069

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 1033	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ 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:  frirrg  4495  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ordiso2  7375  addlocpr  7903  aptiprlemu  8007  xltadd1  10278  xlesubadd  10285  icoshftf1o  10393  fztri3or  10443  elfzonelfzo  10648  exp3val  10978  nn0ltexp2  11147  hashun  11245  swrdclg  11422  subcn2  12077  divalglemeuneg  12690  dvdslegcd  12741  lcmledvds  12848  rpdvds  12877  cncongr2  12882  qexpz  13131  iuncld  15216  iscnp4  15319  cnpnei  15320  cnconst2  15334  cnpdis  15343  txcn  15376  blssps  15528  blss  15529  metcnp3  15612  metcnp  15613  lgsfcl2  16125  lgsdir  16154  lgsne0  16157  eulerpathum  16722