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

Proof

Step Hyp Ref Expression
1 df-3an ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
2 1 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
3 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
4 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
5 4 anbi1i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
6 df-3an ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
7 5 6 bitr4i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
8 2 3 7 3bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )