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 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
2 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
3 1 2 bianbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
4 df-3an ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
5 4 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
6 df-3an ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
7 3 5 6 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )