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  4495  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ordiso2  7375  addlocpr  7903  aptiprlemu  8007  xltadd1  10288  xlesubadd  10295  icoshftf1o  10403  fztri3or  10453  elfzonelfzo  10658  exp3val  10991  nn0ltexp2  11161  hashun  11259  swrdclg  11436  subcn2  12093  divalglemeuneg  12706  dvdslegcd  12757  lcmledvds  12864  rpdvds  12893  cncongr2  12898  qexpz  13151  iuncld  15265  iscnp4  15368  cnpnei  15369  cnconst2  15383  cnpdis  15392  txcn  15425  blssps  15577  blss  15578  metcnp3  15661  metcnp  15662  lgsfcl2  16223  lgsdir  16252  lgsne0  16255  eulerpathum  16820