Theorem simpll3 1065

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

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

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 1007

This theorem is referenced by:  frirrg  4476  fidceq  7137  fidifsnen  7138  en2eqpr  7180  iunfidisj  7226  ordiso2  7339  addlocpr  7867  aptiprlemu  7971  xltadd1  10228  xlesubadd  10235  icoshftf1o  10343  fztri3or  10393  elfzonelfzo  10597  exp3val  10927  nn0ltexp2  11096  hashun  11194  swrdclg  11367  subcn2  12021  divalglemeuneg  12634  dvdslegcd  12685  lcmledvds  12792  rpdvds  12821  cncongr2  12826  qexpz  13075  iuncld  15106  iscnp4  15209  cnpnei  15210  cnconst2  15224  cnpdis  15233  txcn  15266  blssps  15418  blss  15419  metcnp3  15502  metcnp  15503  lgsfcl2  16005  lgsdir  16034  lgsne0  16037  eulerpathum  16602