Theorem simpll2 1064

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  fidceq  7099  fidifsnen  7100  en2eqpr  7142  iunfidisj  7188  ctssdc  7355  cauappcvgprlemlol  7910  caucvgprlemlol  7933  caucvgprprlemlol  7961  elfzonelfzo  10521  qbtwnre  10562  nn0ltexp2  11017  hashun  11114  swrdclg  11280  xrmaxltsup  11881  subcn2  11934  prodmodclem2  12201  divalglemex  12546  divalglemeuneg  12547  dvdslegcd  12598  lcmledvds  12705  modprmn0modprm0  12892  qexpz  12988  rnglidlmcl  14559  iscnp4  15012  cnrest2  15030  blssps  15221  blss  15222  bdbl  15297  metcnp3  15305  addcncntoplem  15355  cdivcncfap  15398  lgsfcl2  15808  lgsdir  15837  lgsne0  15840  subupgr  16197  clwwlknonex2  16363