Theorem simpll3 1062

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

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

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 1004

This theorem is referenced by:  frirrg  4445  fidceq  7051  fidifsnen  7052  en2eqpr  7092  iunfidisj  7136  ordiso2  7225  addlocpr  7746  aptiprlemu  7850  xltadd1  10101  xlesubadd  10108  icoshftf1o  10216  fztri3or  10264  elfzonelfzo  10465  exp3val  10793  nn0ltexp2  10961  hashun  11058  swrdclg  11221  subcn2  11862  divalglemeuneg  12474  dvdslegcd  12525  lcmledvds  12632  rpdvds  12661  cncongr2  12666  qexpz  12915  iuncld  14829  iscnp4  14932  cnpnei  14933  cnconst2  14947  cnpdis  14956  txcn  14989  blssps  15141  blss  15142  metcnp3  15225  metcnp  15226  lgsfcl2  15725  lgsdir  15754  lgsne0  15757