Metamath Proof Explorer


Theorem 2ralbiim

Description: Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim and ralbiim . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Assertion 2ralbiim x A y B φ ψ x A y B φ ψ x A y B ψ φ

Proof

Step Hyp Ref Expression
1 ralbiim y B φ ψ y B φ ψ y B ψ φ
2 1 ralbii x A y B φ ψ x A y B φ ψ y B ψ φ
3 r19.26 x A y B φ ψ y B ψ φ x A y B φ ψ x A y B ψ φ
4 2 3 bitri x A y B φ ψ x A y B φ ψ x A y B ψ φ