Theorem gencl

Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996)

	Ref	Expression
Hypotheses	gencl.1	|- ( th <-> E. x ( ch /\ A = B ) )
	gencl.2	|- ( A = B -> ( ph <-> ps ) )
	gencl.3	|- ( ch -> ph )
Assertion	gencl	|- ( th -> ps )

Proof

Step	Hyp	Ref	Expression
1		gencl.1	|- ( th <-> E. x ( ch /\ A = B ) )
2		gencl.2	|- ( A = B -> ( ph <-> ps ) )
3		gencl.3	|- ( ch -> ph )
4	3 2	syl5ib	|- ( A = B -> ( ch -> ps ) )
5	4	impcom	|- ( ( ch /\ A = B ) -> ps )
6	5	exlimiv	|- ( E. x ( ch /\ A = B ) -> ps )
7	1 6	sylbi	|- ( th -> ps )