Metamath Proof Explorer

Theorem r19.26-3

Description: Version of r19.26 with three quantifiers. (Contributed by FL, 22-Nov-2010)

Ref Expression
Assertion r19.26-3 ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ψ ∧ ∀ x ∈ A χ
2 r19.26 ⊢ ∀ x ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ
3 1 2 bianbi ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ
4 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
5 4 ralbii ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ψ ∧ χ
6 df-3an ⊢ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ
7 3 5 6 3bitr4i ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ