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 | |
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 | |