Theorem simpll3 1041

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

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

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 983

This theorem is referenced by:  frirrg  4415  fidceq  6992  fidifsnen  6993  en2eqpr  7030  iunfidisj  7074  ordiso2  7163  addlocpr  7684  aptiprlemu  7788  xltadd1  10033  xlesubadd  10040  icoshftf1o  10148  fztri3or  10196  elfzonelfzo  10396  exp3val  10723  nn0ltexp2  10891  hashun  10987  swrdclg  11141  subcn2  11737  divalglemeuneg  12349  dvdslegcd  12400  lcmledvds  12507  rpdvds  12536  cncongr2  12541  qexpz  12790  iuncld  14702  iscnp4  14805  cnpnei  14806  cnconst2  14820  cnpdis  14829  txcn  14862  blssps  15014  blss  15015  metcnp3  15098  metcnp  15099  lgsfcl2  15598  lgsdir  15627  lgsne0  15630