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  7175  fidifsnen  7176  en2eqpr  7218  iunfidisj  7264  fdcf1  7321  ctssdc  7459  cauappcvgprlemlol  8020  caucvgprlemlol  8043  caucvgprprlemlol  8071  elfzonelfzo  10665  qbtwnre  10708  nn0ltexp2  11169  hashun  11267  swrdclg  11444  xrmaxltsup  12049  subcn2  12102  prodmodclem2  12369  divalglemex  12714  divalglemeuneg  12715  dvdslegcd  12766  lcmledvds  12873  modprmn0modprm0  13064  qexpz  13160  rnglidlmcl  14926  iscnp4  15444  cnrest2  15462  blssps  15653  blss  15654  bdbl  15729  metcnp3  15737  addcncntoplem  15787  cdivcncfap  15830  lgsfcl2  16330  lgsdir  16359  lgsne0  16362  subupgr  16719  clwwlknonex2  16885