Theorem simpll3 1069

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  frirrg  4497  fidceq  7175  fidifsnen  7176  en2eqpr  7218  iunfidisj  7264  fdcf1  7321  ordiso2  7381  addlocpr  7909  aptiprlemu  8013  xltadd1  10295  xlesubadd  10302  icoshftf1o  10410  fztri3or  10460  elfzonelfzo  10665  exp3val  10999  nn0ltexp2  11169  hashun  11267  swrdclg  11444  subcn2  12102  divalglemeuneg  12715  dvdslegcd  12766  lcmledvds  12873  rpdvds  12902  cncongr2  12907  qexpz  13160  iuncld  15341  iscnp4  15444  cnpnei  15445  cnconst2  15459  cnpdis  15468  txcn  15501  blssps  15653  blss  15654  metcnp3  15737  metcnp  15738  lgsfcl2  16330  lgsdir  16359  lgsne0  16362  eulerpathum  16927