Theorem simpll3 1033

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

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

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 975

This theorem is referenced by:  frirrg  4335  fidceq  6847  fidifsnen  6848  en2eqpr  6885  iunfidisj  6923  ordiso2  7012  addlocpr  7498  aptiprlemu  7602  xltadd1  9833  xlesubadd  9840  icoshftf1o  9948  fztri3or  9995  elfzonelfzo  10186  exp3val  10478  nn0ltexp2  10644  hashun  10740  subcn2  11274  divalglemeuneg  11882  dvdslegcd  11919  lcmledvds  12024  rpdvds  12053  cncongr2  12058  qexpz  12304  iuncld  12909  iscnp4  13012  cnpnei  13013  cnconst2  13027  cnpdis  13036  txcn  13069  blssps  13221  blss  13222  metcnp3  13305  metcnp  13306  lgsfcl2  13701  lgsdir  13730  lgsne0  13733