Theorem simpll3 1069

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

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

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 1011

This theorem is referenced by:  frirrg  4490  fidceq  7161  fidifsnen  7162  en2eqpr  7204  iunfidisj  7250  fdcf1  7306  ordiso2  7365  addlocpr  7893  aptiprlemu  7997  xltadd1  10257  xlesubadd  10264  icoshftf1o  10372  fztri3or  10422  elfzonelfzo  10626  exp3val  10956  nn0ltexp2  11125  hashun  11223  swrdclg  11400  subcn2  12055  divalglemeuneg  12668  dvdslegcd  12719  lcmledvds  12826  rpdvds  12855  cncongr2  12860  qexpz  13109  iuncld  15139  iscnp4  15242  cnpnei  15243  cnconst2  15257  cnpdis  15266  txcn  15299  blssps  15451  blss  15452  metcnp3  15535  metcnp  15536  lgsfcl2  16039  lgsdir  16068  lgsne0  16071  eulerpathum  16636