Theorem bj-19.41al

Description: Special case of 19.41 proved from core axioms, ax-10 (modal5), and hba1 (modal4). (Contributed by BJ, 29-Dec-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-19.41al	|- ( E. x ( ph /\ A. x ps ) <-> ( E. x ph /\ A. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.40	|- ( E. x ( ph /\ A. x ps ) -> ( E. x ph /\ E. x A. x ps ) )
2		hbe1a	|- ( E. x A. x ps -> A. x ps )
3	2	anim2i	|- ( ( E. x ph /\ E. x A. x ps ) -> ( E. x ph /\ A. x ps ) )
4	1 3	syl	|- ( E. x ( ph /\ A. x ps ) -> ( E. x ph /\ A. x ps ) )
5		hba1	|- ( A. x ps -> A. x A. x ps )
6	5	anim2i	|- ( ( E. x ph /\ A. x ps ) -> ( E. x ph /\ A. x A. x ps ) )
7		19.29r	|- ( ( E. x ph /\ A. x A. x ps ) -> E. x ( ph /\ A. x ps ) )
8	6 7	syl	|- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ A. x ps ) )
9	4 8	impbii	|- ( E. x ( ph /\ A. x ps ) <-> ( E. x ph /\ A. x ps ) )