Theorem simpll3 1040

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

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

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 982

This theorem is referenced by:  frirrg  4396  fidceq  6965  fidifsnen  6966  en2eqpr  7003  iunfidisj  7047  ordiso2  7136  addlocpr  7648  aptiprlemu  7752  xltadd1  9997  xlesubadd  10004  icoshftf1o  10112  fztri3or  10160  elfzonelfzo  10357  exp3val  10684  nn0ltexp2  10852  hashun  10948  subcn2  11593  divalglemeuneg  12205  dvdslegcd  12256  lcmledvds  12363  rpdvds  12392  cncongr2  12397  qexpz  12646  iuncld  14558  iscnp4  14661  cnpnei  14662  cnconst2  14676  cnpdis  14685  txcn  14718  blssps  14870  blss  14871  metcnp3  14954  metcnp  14955  lgsfcl2  15454  lgsdir  15483  lgsne0  15486