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 ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.26 ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )