Metamath Proof Explorer

Theorem 2albiim

Description: Split a biconditional and distribute two quantifiers. (Contributed by NM, 3-Feb-2005)

Ref Expression
Assertion 2albiim ⊢ ∀ x ∀ y φ ↔ ψ ↔ ∀ x ∀ y φ → ψ ∧ ∀ x ∀ y ψ → φ

Proof

Step Hyp Ref Expression
1 albiim ⊢ ∀ y φ ↔ ψ ↔ ∀ y φ → ψ ∧ ∀ y ψ → φ
2 1 albii ⊢ ∀ x ∀ y φ ↔ ψ ↔ ∀ x ∀ y φ → ψ ∧ ∀ y ψ → φ
3 19.26 ⊢ ∀ x ∀ y φ → ψ ∧ ∀ y ψ → φ ↔ ∀ x ∀ y φ → ψ ∧ ∀ x ∀ y ψ → φ
4 2 3 bitri ⊢ ∀ x ∀ y φ ↔ ψ ↔ ∀ x ∀ y φ → ψ ∧ ∀ x ∀ y ψ → φ