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	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜓 ↔ ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) )

Metamath Proof Explorer

Theorem raltpd

Proof