Theorem simpll3 1062

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

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

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 1004

This theorem is referenced by:  frirrg  4440  fidceq  7027  fidifsnen  7028  en2eqpr  7065  iunfidisj  7109  ordiso2  7198  addlocpr  7719  aptiprlemu  7823  xltadd1  10068  xlesubadd  10075  icoshftf1o  10183  fztri3or  10231  elfzonelfzo  10431  exp3val  10758  nn0ltexp2  10926  hashun  11022  swrdclg  11177  subcn2  11817  divalglemeuneg  12429  dvdslegcd  12480  lcmledvds  12587  rpdvds  12616  cncongr2  12621  qexpz  12870  iuncld  14783  iscnp4  14886  cnpnei  14887  cnconst2  14901  cnpdis  14910  txcn  14943  blssps  15095  blss  15096  metcnp3  15179  metcnp  15180  lgsfcl2  15679  lgsdir  15708  lgsne0  15711