Metamath Proof Explorer


Theorem 2ralbidv

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006) (Revised by Szymon Jaroszewicz, 16-Mar-2007)

Ref Expression
Hypothesis 2ralbidv.1 φψχ
Assertion 2ralbidv φxAyBψxAyBχ

Proof

Step Hyp Ref Expression
1 2ralbidv.1 φψχ
2 1 ralbidv φyBψyBχ
3 2 ralbidv φxAyBψxAyBχ