Theorem ralbidc

Description: Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb . (Contributed by Zhi Wang, 30-Aug-2024)

	Ref	Expression
Hypotheses	ralbidb.1	|- ( ph -> ( x e. A <-> ( x e. B /\ ps ) ) )
	ralbidc.2	|- ( ph -> ( ( x e. A /\ ( x e. B /\ ps ) ) -> ( ch <-> th ) ) )
Assertion	ralbidc	|- ( ph -> ( A. x e. A ch <-> A. x e. B ( ps -> th ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralbidb.1	|- ( ph -> ( x e. A <-> ( x e. B /\ ps ) ) )
2		ralbidc.2	|- ( ph -> ( ( x e. A /\ ( x e. B /\ ps ) ) -> ( ch <-> th ) ) )
3	1 2	logic2	|- ( ph -> ( ( x e. A -> ch ) <-> ( ( x e. B /\ ps ) -> th ) ) )
4		impexp	|- ( ( ( x e. B /\ ps ) -> th ) <-> ( x e. B -> ( ps -> th ) ) )
5	3 4	bitrdi	|- ( ph -> ( ( x e. A -> ch ) <-> ( x e. B -> ( ps -> th ) ) ) )
6	5	ralbidv2	|- ( ph -> ( A. x e. A ch <-> A. x e. B ( ps -> th ) ) )