Metamath Proof Explorer

Theorem 19.26-3an

Description: Theorem 19.26 with triple conjunction. (Contributed by NM, 13-Sep-2011)

Ref Expression
Assertion 19.26-3an ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ∧ ∀ 𝑥 𝜒 ) )

Proof

Step Hyp Ref Expression
1 19.26 ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )
2 1 anbi1i ⊢ ( ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 𝜒 ) ↔ ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) ∧ ∀ 𝑥 𝜒 ) )
3 df-3an ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
4 3 albii ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ∀ 𝑥 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
5 19.26 ⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 𝜒 ) )
6 4 5 bitri ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 𝜒 ) )
7 df-3an ⊢ ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ∧ ∀ 𝑥 𝜒 ) ↔ ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) ∧ ∀ 𝑥 𝜒 ) )
8 2 6 7 3bitr4i ⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ∧ ∀ 𝑥 𝜒 ) )