Theorem simpll3 1023

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

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

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

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

This theorem is referenced by:  frirrg  4280  fidceq  6771  fidifsnen  6772  en2eqpr  6809  iunfidisj  6842  ordiso2  6928  addlocpr  7368  aptiprlemu  7472  xltadd1  9689  xlesubadd  9696  icoshftf1o  9804  fztri3or  9850  elfzonelfzo  10038  exp3val  10326  hashun  10583  subcn2  11112  divalglemeuneg  11656  dvdslegcd  11689  lcmledvds  11787  rpdvds  11816  cncongr2  11821  iuncld  12323  iscnp4  12426  cnpnei  12427  cnconst2  12441  cnpdis  12450  txcn  12483  blssps  12635  blss  12636  metcnp3  12719  metcnp  12720