Metamath Proof Explorer


Theorem 4ralbii

Description: Inference adding four restricted universal quantifiers to both sides of an equivalence. (Contributed by Scott Fenton, 28-Feb-2025)

Ref Expression
Hypothesis 4ralbii.1 ( 𝜑𝜓 )
Assertion 4ralbii ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷 𝜑 ↔ ∀ 𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷 𝜓 )

Proof

Step Hyp Ref Expression
1 4ralbii.1 ( 𝜑𝜓 )
2 1 ralbii ( ∀ 𝑤𝐷 𝜑 ↔ ∀ 𝑤𝐷 𝜓 )
3 2 3ralbii ( ∀ 𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷 𝜑 ↔ ∀ 𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷 𝜓 )