Theorem simpll3 1022

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  frirrg  4267  fidceq  6756  fidifsnen  6757  en2eqpr  6794  iunfidisj  6827  ordiso2  6913  addlocpr  7337  aptiprlemu  7441  xltadd1  9652  xlesubadd  9659  icoshftf1o  9767  fztri3or  9812  elfzonelfzo  10000  exp3val  10288  hashun  10544  subcn2  11073  divalglemeuneg  11609  dvdslegcd  11642  lcmledvds  11740  rpdvds  11769  cncongr2  11774  iuncld  12273  iscnp4  12376  cnpnei  12377  cnconst2  12391  cnpdis  12400  txcn  12433  blssps  12585  blss  12586  metcnp3  12669  metcnp  12670