Metamath Proof Explorer

Theorem albiim

Description: Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993)

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

Proof

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