Metamath Proof Explorer

Theorem 19.26

Description: Theorem 19.26 of Margaris p. 90. Also Theorem *10.22 of WhiteheadRussell p. 147. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 4-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 1 alimi ⊢ ∀ x φ ∧ ψ → ∀ x φ
3 simpr ⊢ φ ∧ ψ → ψ
4 3 alimi ⊢ ∀ x φ ∧ ψ → ∀ x ψ
5 2 4 jca ⊢ ∀ x φ ∧ ψ → ∀ x φ ∧ ∀ x ψ
6 id ⊢ φ ∧ ψ → φ ∧ ψ
7 6 alanimi ⊢ ∀ x φ ∧ ∀ x ψ → ∀ x φ ∧ ψ
8 5 7 impbii ⊢ ∀ x φ ∧ ψ ↔ ∀ x φ ∧ ∀ x ψ