Theorem simpll3 1022

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

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

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 964

This theorem is referenced by:  frirrg  4272  fidceq  6763  fidifsnen  6764  en2eqpr  6801  iunfidisj  6834  ordiso2  6920  addlocpr  7344  aptiprlemu  7448  xltadd1  9659  xlesubadd  9666  icoshftf1o  9774  fztri3or  9819  elfzonelfzo  10007  exp3val  10295  hashun  10551  subcn2  11080  divalglemeuneg  11620  dvdslegcd  11653  lcmledvds  11751  rpdvds  11780  cncongr2  11785  iuncld  12284  iscnp4  12387  cnpnei  12388  cnconst2  12402  cnpdis  12411  txcn  12444  blssps  12596  blss  12597  metcnp3  12680  metcnp  12681