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  7124  fidifsnen  7125  en2eqpr  7167  iunfidisj  7213  ctssdc  7404  cauappcvgprlemlol  7962  caucvgprlemlol  7985  caucvgprprlemlol  8013  elfzonelfzo  10575  qbtwnre  10616  nn0ltexp2  11071  hashun  11169  swrdclg  11342  xrmaxltsup  11943  subcn2  11996  prodmodclem2  12263  divalglemex  12608  divalglemeuneg  12609  dvdslegcd  12660  lcmledvds  12767  modprmn0modprm0  12954  qexpz  13050  rnglidlmcl  14628  iscnp4  15083  cnrest2  15101  blssps  15292  blss  15293  bdbl  15368  metcnp3  15376  addcncntoplem  15426  cdivcncfap  15469  lgsfcl2  15879  lgsdir  15908  lgsne0  15911  subupgr  16268  clwwlknonex2  16434