Theorem simpll2 1039

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

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

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 982

This theorem is referenced by:  fidceq  6939  fidifsnen  6940  en2eqpr  6977  iunfidisj  7021  ctssdc  7188  cauappcvgprlemlol  7731  caucvgprlemlol  7754  caucvgprprlemlol  7782  elfzonelfzo  10323  qbtwnre  10363  nn0ltexp2  10818  hashun  10914  xrmaxltsup  11440  subcn2  11493  prodmodclem2  11759  divalglemex  12104  divalglemeuneg  12105  dvdslegcd  12156  lcmledvds  12263  modprmn0modprm0  12450  qexpz  12546  rnglidlmcl  14112  iscnp4  14538  cnrest2  14556  blssps  14747  blss  14748  bdbl  14823  metcnp3  14831  addcncntoplem  14881  cdivcncfap  14924  lgsfcl2  15331  lgsdir  15360  lgsne0  15363