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 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
2 1 ralbii ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ψ ∧ χ
3 r19.26 ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ψ ∧ ∀ x ∈ A χ
4 r19.26 ⊢ ∀ x ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ
5 4 anbi1i ⊢ ∀ x ∈ A φ ∧ ψ ∧ ∀ x ∈ A χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ
6 df-3an ⊢ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ
7 5 6 bitr4i ⊢ ∀ x ∈ A φ ∧ ψ ∧ ∀ x ∈ A χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ
8 2 3 7 3bitri ⊢ ∀ x ∈ A φ ∧ ψ ∧ χ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ x ∈ A χ