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  4453  fidceq  7099  fidifsnen  7100  en2eqpr  7142  iunfidisj  7188  ordiso2  7277  addlocpr  7799  aptiprlemu  7903  xltadd1  10155  xlesubadd  10162  icoshftf1o  10270  fztri3or  10319  elfzonelfzo  10521  exp3val  10849  nn0ltexp2  11017  hashun  11114  swrdclg  11280  subcn2  11934  divalglemeuneg  12547  dvdslegcd  12598  lcmledvds  12705  rpdvds  12734  cncongr2  12739  qexpz  12988  iuncld  14909  iscnp4  15012  cnpnei  15013  cnconst2  15027  cnpdis  15036  txcn  15069  blssps  15221  blss  15222  metcnp3  15305  metcnp  15306  lgsfcl2  15808  lgsdir  15837  lgsne0  15840  eulerpathum  16405