This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2albii

Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997)

Ref Expression
Hypothesis albii.1 ⊢ φ ↔ ψ
Assertion 2albii ⊢ ∀ x ∀ y φ ↔ ∀ x ∀ y ψ

Proof

Step Hyp Ref Expression
1 albii.1 ⊢ φ ↔ ψ
2 1 albii ⊢ ∀ y φ ↔ ∀ y ψ
3 2 albii ⊢ ∀ x ∀ y φ ↔ ∀ x ∀ y ψ