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  4310  fidceq  6814  fidifsnen  6815  en2eqpr  6852  iunfidisj  6890  ordiso2  6979  addlocpr  7456  aptiprlemu  7560  xltadd1  9780  xlesubadd  9787  icoshftf1o  9895  fztri3or  9941  elfzonelfzo  10129  exp3val  10421  hashun  10679  subcn2  11208  divalglemeuneg  11814  dvdslegcd  11848  lcmledvds  11947  rpdvds  11976  cncongr2  11981  iuncld  12526  iscnp4  12629  cnpnei  12630  cnconst2  12644  cnpdis  12653  txcn  12686  blssps  12838  blss  12839  metcnp3  12922  metcnp  12923