Metamath Proof Explorer

Theorem raltpd

Description: Convert a universal quantification over an unordered triple to a conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019)

Ref Expression
Hypotheses ralprd.1 ⊢ φ ∧ x = A → ψ ↔ χ
ralprd.2 ⊢ φ ∧ x = B → ψ ↔ θ
raltpd.3 ⊢ φ ∧ x = C → ψ ↔ τ
ralprd.a ⊢ φ → A ∈ V
ralprd.b ⊢ φ → B ∈ W
raltpd.c ⊢ φ → C ∈ X
Assertion raltpd ⊢ φ → ∀ x ∈ A B C ψ ↔ χ ∧ θ ∧ τ

Proof

Step Hyp Ref Expression
1 ralprd.1 ⊢ φ ∧ x = A → ψ ↔ χ
2 ralprd.2 ⊢ φ ∧ x = B → ψ ↔ θ
3 raltpd.3 ⊢ φ ∧ x = C → ψ ↔ τ
4 ralprd.a ⊢ φ → A ∈ V
5 ralprd.b ⊢ φ → B ∈ W
6 raltpd.c ⊢ φ → C ∈ X
7 an3andi ⊢ φ ∧ χ ∧ θ ∧ τ ↔ φ ∧ χ ∧ φ ∧ θ ∧ φ ∧ τ
8 7 a1i ⊢ φ → φ ∧ χ ∧ θ ∧ τ ↔ φ ∧ χ ∧ φ ∧ θ ∧ φ ∧ τ
9 1 expcom ⊢ x = A → φ → ψ ↔ χ
10 9 pm5.32d ⊢ x = A → φ ∧ ψ ↔ φ ∧ χ
11 2 expcom ⊢ x = B → φ → ψ ↔ θ
12 11 pm5.32d ⊢ x = B → φ ∧ ψ ↔ φ ∧ θ
13 3 expcom ⊢ x = C → φ → ψ ↔ τ
14 13 pm5.32d ⊢ x = C → φ ∧ ψ ↔ φ ∧ τ
15 10 12 14 raltpg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∀ x ∈ A B C φ ∧ ψ ↔ φ ∧ χ ∧ φ ∧ θ ∧ φ ∧ τ
16 4 5 6 15 syl3anc ⊢ φ → ∀ x ∈ A B C φ ∧ ψ ↔ φ ∧ χ ∧ φ ∧ θ ∧ φ ∧ τ
17 4 tpnzd ⊢ φ → A B C ≠ ∅
18 r19.28zv ⊢ A B C ≠ ∅ → ∀ x ∈ A B C φ ∧ ψ ↔ φ ∧ ∀ x ∈ A B C ψ
19 17 18 syl ⊢ φ → ∀ x ∈ A B C φ ∧ ψ ↔ φ ∧ ∀ x ∈ A B C ψ
20 8 16 19 3bitr2d ⊢ φ → φ ∧ χ ∧ θ ∧ τ ↔ φ ∧ ∀ x ∈ A B C ψ
21 20 bianabs ⊢ φ → φ ∧ χ ∧ θ ∧ τ ↔ ∀ x ∈ A B C ψ
22 21 bicomd ⊢ φ → ∀ x ∈ A B C ψ ↔ φ ∧ χ ∧ θ ∧ τ
23 22 bianabs ⊢ φ → ∀ x ∈ A B C ψ ↔ χ ∧ θ ∧ τ