Theorem pm2.61danel 2911

Description: Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.)

Hypotheses

Ref	Expression
pm2.61danel.1	|- ( ( ph /\ A e. B ) -> ps )
pm2.61danel.2	|- ( ( ph /\ A e/ B ) -> ps )

Assertion

Ref	Expression
pm2.61danel	|- ( ph -> ps )

Proof of Theorem pm2.61danel

Step	Hyp	Ref	Expression
1		pm2.61danel.1	. 2 |- ( ( ph /\ A e. B ) -> ps )
2		df-nel 2898	. . 3 |- ( A e/ B <-> -. A e. B )
3		pm2.61danel.2	. . 3 |- ( ( ph /\ A e/ B ) -> ps )
4	2, 3	sylan2br 493	. 2 |- ( ( ph /\ -. A e. B ) -> ps )
5	1, 4	pm2.61dan 832	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   e. wcel 1990   e/ wnel 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-nel 2898

This theorem is referenced by:  nsnlpligALT  27334  n0lpligALT  27336