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  4352  fidceq  6871  fidifsnen  6872  en2eqpr  6909  iunfidisj  6947  ordiso2  7036  addlocpr  7537  aptiprlemu  7641  xltadd1  9878  xlesubadd  9885  icoshftf1o  9993  fztri3or  10041  elfzonelfzo  10232  exp3val  10524  nn0ltexp2  10691  hashun  10787  subcn2  11321  divalglemeuneg  11930  dvdslegcd  11967  lcmledvds  12072  rpdvds  12101  cncongr2  12106  qexpz  12352  iuncld  13654  iscnp4  13757  cnpnei  13758  cnconst2  13772  cnpdis  13781  txcn  13814  blssps  13966  blss  13967  metcnp3  14050  metcnp  14051  lgsfcl2  14446  lgsdir  14475  lgsne0  14478