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  4471  fidceq  7124  fidifsnen  7125  en2eqpr  7167  iunfidisj  7213  ordiso2  7326  addlocpr  7851  aptiprlemu  7955  xltadd1  10209  xlesubadd  10216  icoshftf1o  10324  fztri3or  10373  elfzonelfzo  10575  exp3val  10903  nn0ltexp2  11071  hashun  11169  swrdclg  11342  subcn2  11996  divalglemeuneg  12609  dvdslegcd  12660  lcmledvds  12767  rpdvds  12796  cncongr2  12801  qexpz  13050  iuncld  14980  iscnp4  15083  cnpnei  15084  cnconst2  15098  cnpdis  15107  txcn  15140  blssps  15292  blss  15293  metcnp3  15376  metcnp  15377  lgsfcl2  15879  lgsdir  15908  lgsne0  15911  eulerpathum  16476