Theorem simpll3 1040

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

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

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 982

This theorem is referenced by:  frirrg  4382  fidceq  6927  fidifsnen  6928  en2eqpr  6965  iunfidisj  7007  ordiso2  7096  addlocpr  7598  aptiprlemu  7702  xltadd1  9945  xlesubadd  9952  icoshftf1o  10060  fztri3or  10108  elfzonelfzo  10300  exp3val  10615  nn0ltexp2  10783  hashun  10879  subcn2  11457  divalglemeuneg  12067  dvdslegcd  12104  lcmledvds  12211  rpdvds  12240  cncongr2  12245  qexpz  12493  iuncld  14294  iscnp4  14397  cnpnei  14398  cnconst2  14412  cnpdis  14421  txcn  14454  blssps  14606  blss  14607  metcnp3  14690  metcnp  14691  lgsfcl2  15163  lgsdir  15192  lgsne0  15195