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 
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
ralprd.2 
|- ( ( ph /\ x = B ) -> ( ps <-> th ) )
raltpd.3 
|- ( ( ph /\ x = C ) -> ( ps <-> ta ) )
ralprd.a 
|- ( ph -> A e. V )
ralprd.b 
|- ( ph -> B e. W )
raltpd.c 
|- ( ph -> C e. X )
Assertion raltpd 
|- ( ph -> ( A. x e. { A , B , C } ps <-> ( ch /\ th /\ ta ) ) )

Proof

Step Hyp Ref Expression
1 ralprd.1 
 |-  ( ( ph /\ x = A ) -> ( ps <-> ch ) )
2 ralprd.2 
 |-  ( ( ph /\ x = B ) -> ( ps <-> th ) )
3 raltpd.3 
 |-  ( ( ph /\ x = C ) -> ( ps <-> ta ) )
4 ralprd.a 
 |-  ( ph -> A e. V )
5 ralprd.b 
 |-  ( ph -> B e. W )
6 raltpd.c 
 |-  ( ph -> C e. X )
7 an3andi 
 |-  ( ( ph /\ ( ch /\ th /\ ta ) ) <-> ( ( ph /\ ch ) /\ ( ph /\ th ) /\ ( ph /\ ta ) ) )
8 7 a1i 
 |-  ( ph -> ( ( ph /\ ( ch /\ th /\ ta ) ) <-> ( ( ph /\ ch ) /\ ( ph /\ th ) /\ ( ph /\ ta ) ) ) )
9 1 expcom 
 |-  ( x = A -> ( ph -> ( ps <-> ch ) ) )
10 9 pm5.32d 
 |-  ( x = A -> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
11 2 expcom 
 |-  ( x = B -> ( ph -> ( ps <-> th ) ) )
12 11 pm5.32d 
 |-  ( x = B -> ( ( ph /\ ps ) <-> ( ph /\ th ) ) )
13 3 expcom 
 |-  ( x = C -> ( ph -> ( ps <-> ta ) ) )
14 13 pm5.32d 
 |-  ( x = C -> ( ( ph /\ ps ) <-> ( ph /\ ta ) ) )
15 10 12 14 raltpg 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. x e. { A , B , C } ( ph /\ ps ) <-> ( ( ph /\ ch ) /\ ( ph /\ th ) /\ ( ph /\ ta ) ) ) )
16 4 5 6 15 syl3anc 
 |-  ( ph -> ( A. x e. { A , B , C } ( ph /\ ps ) <-> ( ( ph /\ ch ) /\ ( ph /\ th ) /\ ( ph /\ ta ) ) ) )
17 4 tpnzd 
 |-  ( ph -> { A , B , C } =/= (/) )
18 r19.28zv 
 |-  ( { A , B , C } =/= (/) -> ( A. x e. { A , B , C } ( ph /\ ps ) <-> ( ph /\ A. x e. { A , B , C } ps ) ) )
19 17 18 syl 
 |-  ( ph -> ( A. x e. { A , B , C } ( ph /\ ps ) <-> ( ph /\ A. x e. { A , B , C } ps ) ) )
20 8 16 19 3bitr2d 
 |-  ( ph -> ( ( ph /\ ( ch /\ th /\ ta ) ) <-> ( ph /\ A. x e. { A , B , C } ps ) ) )
21 20 bianabs 
 |-  ( ph -> ( ( ph /\ ( ch /\ th /\ ta ) ) <-> A. x e. { A , B , C } ps ) )
22 21 bicomd 
 |-  ( ph -> ( A. x e. { A , B , C } ps <-> ( ph /\ ( ch /\ th /\ ta ) ) ) )
23 22 bianabs 
 |-  ( ph -> ( A. x e. { A , B , C } ps <-> ( ch /\ th /\ ta ) ) )