Theorem simpll2 1068

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll2	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 1032	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

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

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

This theorem is used by:  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ctssdc  7454  cauappcvgprlemlol  8015  caucvgprlemlol  8038  caucvgprprlemlol  8066  elfzonelfzo  10659  qbtwnre  10702  nn0ltexp2  11163  hashun  11261  swrdclg  11438  xrmaxltsup  12043  subcn2  12096  prodmodclem2  12363  divalglemex  12708  divalglemeuneg  12709  dvdslegcd  12760  lcmledvds  12867  modprmn0modprm0  13058  qexpz  13154  rnglidlmcl  14901  iscnp4  15410  cnrest2  15428  blssps  15619  blss  15620  bdbl  15695  metcnp3  15703  addcncntoplem  15753  cdivcncfap  15796  lgsfcl2  16291  lgsdir  16320  lgsne0  16323  subupgr  16680  clwwlknonex2  16846