Theorem simpll3 1040

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 1004	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ 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:  frirrg  4386  fidceq  6939  fidifsnen  6940  en2eqpr  6977  iunfidisj  7021  ordiso2  7110  addlocpr  7620  aptiprlemu  7724  xltadd1  9968  xlesubadd  9975  icoshftf1o  10083  fztri3or  10131  elfzonelfzo  10323  exp3val  10650  nn0ltexp2  10818  hashun  10914  subcn2  11493  divalglemeuneg  12105  dvdslegcd  12156  lcmledvds  12263  rpdvds  12292  cncongr2  12297  qexpz  12546  iuncld  14435  iscnp4  14538  cnpnei  14539  cnconst2  14553  cnpdis  14562  txcn  14595  blssps  14747  blss  14748  metcnp3  14831  metcnp  14832  lgsfcl2  15331  lgsdir  15360  lgsne0  15363