This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.21bi

Description: Inference from Theorem 19.21 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994) (Proof shortened by Wolf Lammen, 11-Jun-2023)

		Ref	Expression
	Hypothesis	r19.21bi.1	\|- ( ph -> A. x e. A ps )
	Assertion	r19.21bi	\|- ( ( ph /\ x e. A ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		r19.21bi.1	\|- ( ph -> A. x e. A ps )
2		rspa	\|- ( ( A. x e. A ps /\ x e. A ) -> ps )
3	1 2	sylan	\|- ( ( ph /\ x e. A ) -> ps )