Theorem simpll3 1069

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  frirrg  4497  fidceq  7177  fidifsnen  7178  en2eqpr  7220  iunfidisj  7266  fdcf1  7321  ordiso2  7381  addlocpr  7909  aptiprlemu  8013  xltadd1  10294  xlesubadd  10301  icoshftf1o  10409  fztri3or  10459  elfzonelfzo  10664  exp3val  10998  nn0ltexp2  11168  hashun  11266  swrdclg  11443  subcn2  12101  divalglemeuneg  12714  dvdslegcd  12765  lcmledvds  12872  rpdvds  12901  cncongr2  12906  qexpz  13159  iuncld  15358  iscnp4  15461  cnpnei  15462  cnconst2  15476  cnpdis  15485  txcn  15518  blssps  15670  blss  15671  metcnp3  15754  metcnp  15755  lgsfcl2  16347  lgsdir  16376  lgsne0  16379  eulerpathum  16944