Theorem simpll3 1038

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 1002	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )

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

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 980

This theorem is referenced by:  frirrg  4350  fidceq  6868  fidifsnen  6869  en2eqpr  6906  iunfidisj  6944  ordiso2  7033  addlocpr  7534  aptiprlemu  7638  xltadd1  9875  xlesubadd  9882  icoshftf1o  9990  fztri3or  10038  elfzonelfzo  10229  exp3val  10521  nn0ltexp2  10688  hashun  10784  subcn2  11318  divalglemeuneg  11927  dvdslegcd  11964  lcmledvds  12069  rpdvds  12098  cncongr2  12103  qexpz  12349  iuncld  13585  iscnp4  13688  cnpnei  13689  cnconst2  13703  cnpdis  13712  txcn  13745  blssps  13897  blss  13898  metcnp3  13981  metcnp  13982  lgsfcl2  14377  lgsdir  14406  lgsne0  14409