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∈ABCψ↔χ∧θ∧τ

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∈ABCφ∧ψ↔φ∧χ∧φ∧θ∧φ∧τ
16 4 5 6 15 syl3anc ⊢φ→∀x∈ABCφ∧ψ↔φ∧χ∧φ∧θ∧φ∧τ
17 4 tpnzd ⊢φ→ABC≠∅
18 r19.28zv ⊢ABC≠∅→∀x∈ABCφ∧ψ↔φ∧∀x∈ABCψ
19 17 18 syl ⊢φ→∀x∈ABCφ∧ψ↔φ∧∀x∈ABCψ
20 8 16 19 3bitr2d ⊢φ→φ∧χ∧θ∧τ↔φ∧∀x∈ABCψ
21 20 bianabs ⊢φ→φ∧χ∧θ∧τ↔∀x∈ABCψ
22 21 bicomd ⊢φ→∀x∈ABCψ↔φ∧χ∧θ∧τ
23 22 bianabs ⊢φ→∀x∈ABCψ↔χ∧θ∧τ