Theorem simpll3 979

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  frirrg  4105  fidceq  6354  fidifsnen  6355  en2eqpr  6380  ordiso2  6446  addlocpr  6726  aptiprlemu  6830  icoshftf1o  9013  fztri3or  9058  elfzonelfzo  9239  expival  9478  subcn2  10150  divalglemeuneg  10323  dvdslegcd  10356  lcmledvds  10452  rpdvds  10481  cncongr2  10486