Theorem simpll3 1064

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

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

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 1006

This theorem is referenced by:  frirrg  4447  fidceq  7056  fidifsnen  7057  en2eqpr  7099  iunfidisj  7145  ordiso2  7234  addlocpr  7756  aptiprlemu  7860  xltadd1  10111  xlesubadd  10118  icoshftf1o  10226  fztri3or  10274  elfzonelfzo  10476  exp3val  10804  nn0ltexp2  10972  hashun  11069  swrdclg  11235  subcn2  11889  divalglemeuneg  12502  dvdslegcd  12553  lcmledvds  12660  rpdvds  12689  cncongr2  12694  qexpz  12943  iuncld  14858  iscnp4  14961  cnpnei  14962  cnconst2  14976  cnpdis  14985  txcn  15018  blssps  15170  blss  15171  metcnp3  15254  metcnp  15255  lgsfcl2  15754  lgsdir  15783  lgsne0  15786  eulerpathum  16351