Theorem simpll3 1038

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

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

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 980

This theorem is referenced by:  frirrg  4350  fidceq  6868  fidifsnen  6869  en2eqpr  6906  iunfidisj  6944  ordiso2  7033  addlocpr  7534  aptiprlemu  7638  xltadd1  9874  xlesubadd  9881  icoshftf1o  9989  fztri3or  10036  elfzonelfzo  10227  exp3val  10519  nn0ltexp2  10685  hashun  10780  subcn2  11314  divalglemeuneg  11922  dvdslegcd  11959  lcmledvds  12064  rpdvds  12093  cncongr2  12098  qexpz  12344  iuncld  13508  iscnp4  13611  cnpnei  13612  cnconst2  13626  cnpdis  13635  txcn  13668  blssps  13820  blss  13821  metcnp3  13904  metcnp  13905  lgsfcl2  14300  lgsdir  14329  lgsne0  14332