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χ