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 ( ( 𝜑𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
ralprd.2 ( ( 𝜑𝑥 = 𝐵 ) → ( 𝜓𝜃 ) )
raltpd.3 ( ( 𝜑𝑥 = 𝐶 ) → ( 𝜓𝜏 ) )
ralprd.a ( 𝜑𝐴𝑉 )
ralprd.b ( 𝜑𝐵𝑊 )
raltpd.c ( 𝜑𝐶𝑋 )
Assertion raltpd ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ↔ ( 𝜒𝜃𝜏 ) ) )

Proof

Step Hyp Ref Expression
1 ralprd.1 ( ( 𝜑𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
2 ralprd.2 ( ( 𝜑𝑥 = 𝐵 ) → ( 𝜓𝜃 ) )
3 raltpd.3 ( ( 𝜑𝑥 = 𝐶 ) → ( 𝜓𝜏 ) )
4 ralprd.a ( 𝜑𝐴𝑉 )
5 ralprd.b ( 𝜑𝐵𝑊 )
6 raltpd.c ( 𝜑𝐶𝑋 )
7 an3andi ( ( 𝜑 ∧ ( 𝜒𝜃𝜏 ) ) ↔ ( ( 𝜑𝜒 ) ∧ ( 𝜑𝜃 ) ∧ ( 𝜑𝜏 ) ) )
8 7 a1i ( 𝜑 → ( ( 𝜑 ∧ ( 𝜒𝜃𝜏 ) ) ↔ ( ( 𝜑𝜒 ) ∧ ( 𝜑𝜃 ) ∧ ( 𝜑𝜏 ) ) ) )
9 1 expcom ( 𝑥 = 𝐴 → ( 𝜑 → ( 𝜓𝜒 ) ) )
10 9 pm5.32d ( 𝑥 = 𝐴 → ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜒 ) ) )
11 2 expcom ( 𝑥 = 𝐵 → ( 𝜑 → ( 𝜓𝜃 ) ) )
12 11 pm5.32d ( 𝑥 = 𝐵 → ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜃 ) ) )
13 3 expcom ( 𝑥 = 𝐶 → ( 𝜑 → ( 𝜓𝜏 ) ) )
14 13 pm5.32d ( 𝑥 = 𝐶 → ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜏 ) ) )
15 10 12 14 raltpg ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ( 𝜑𝜓 ) ↔ ( ( 𝜑𝜒 ) ∧ ( 𝜑𝜃 ) ∧ ( 𝜑𝜏 ) ) ) )
16 4 5 6 15 syl3anc ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ( 𝜑𝜓 ) ↔ ( ( 𝜑𝜒 ) ∧ ( 𝜑𝜃 ) ∧ ( 𝜑𝜏 ) ) ) )
17 4 tpnzd ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )
18 r19.28zv ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ( 𝜑𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ) ) )
19 17 18 syl ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ( 𝜑𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ) ) )
20 8 16 19 3bitr2d ( 𝜑 → ( ( 𝜑 ∧ ( 𝜒𝜃𝜏 ) ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ) ) )
21 20 bianabs ( 𝜑 → ( ( 𝜑 ∧ ( 𝜒𝜃𝜏 ) ) ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ) )
22 21 bicomd ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ↔ ( 𝜑 ∧ ( 𝜒𝜃𝜏 ) ) ) )
23 22 bianabs ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ↔ ( 𝜒𝜃𝜏 ) ) )