Metamath Proof Explorer


Theorem 3albii

Description: Inference adding three universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 10-Aug-2018)

Ref Expression
Hypothesis 3albii.1 ( 𝜑𝜓 )
Assertion 3albii ( ∀ 𝑥𝑦𝑧 𝜑 ↔ ∀ 𝑥𝑦𝑧 𝜓 )

Proof

Step Hyp Ref Expression
1 3albii.1 ( 𝜑𝜓 )
2 1 2albii ( ∀ 𝑦𝑧 𝜑 ↔ ∀ 𝑦𝑧 𝜓 )
3 2 albii ( ∀ 𝑥𝑦𝑧 𝜑 ↔ ∀ 𝑥𝑦𝑧 𝜓 )