Theorem simpll3 1028

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

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

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 970

This theorem is referenced by:  frirrg  4327  fidceq  6831  fidifsnen  6832  en2eqpr  6869  iunfidisj  6907  ordiso2  6996  addlocpr  7473  aptiprlemu  7577  xltadd1  9808  xlesubadd  9815  icoshftf1o  9923  fztri3or  9970  elfzonelfzo  10161  exp3val  10453  nn0ltexp2  10619  hashun  10714  subcn2  11248  divalglemeuneg  11856  dvdslegcd  11893  lcmledvds  11998  rpdvds  12027  cncongr2  12032  qexpz  12278  iuncld  12715  iscnp4  12818  cnpnei  12819  cnconst2  12833  cnpdis  12842  txcn  12875  blssps  13027  blss  13028  metcnp3  13111  metcnp  13112  lgsfcl2  13507  lgsdir  13536  lgsne0  13539