Metamath Proof Explorer


Theorem alan

Description: Alias for 19.26 for easier lookup. (Contributed by SN, 12-Aug-2025) (New usage is discouraged.)

Ref Expression
Assertion alan ⊢ ∀ x φ ∧ ψ ↔ ∀ x φ ∧ ∀ x ψ

Proof

Step Hyp Ref Expression
1 19.26 ⊢ ∀ x φ ∧ ψ ↔ ∀ x φ ∧ ∀ x ψ