Theorem simpll3 985

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 925

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

This theorem depends on definitions:  df-bi 116  df-3an 927

This theorem is referenced by:  frirrg  4188  fidceq  6641  fidifsnen  6642  en2eqpr  6679  iunfidisj  6711  ordiso2  6784  addlocpr  7158  aptiprlemu  7262  icoshftf1o  9471  fztri3or  9516  elfzonelfzo  9704  exp3val  10020  hashun  10276  subcn2  10763  divalglemeuneg  11264  dvdslegcd  11297  lcmledvds  11393  rpdvds  11422  cncongr2  11427  iuncld  11878