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 φAV
ralprd.b φBW
raltpd.c φCX
Assertion raltpd φxABCψχθτ

Proof

Step Hyp Ref Expression
1 ralprd.1 φx=Aψχ
2 ralprd.2 φx=Bψθ
3 raltpd.3 φx=Cψτ
4 ralprd.a φAV
5 ralprd.b φBW
6 raltpd.c φCX
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 AVBWCXxABCφψφχφθφτ
16 4 5 6 15 syl3anc φxABCφψφχφθφτ
17 4 tpnzd φABC
18 r19.28zv ABCxABCφψφxABCψ
19 17 18 syl φxABCφψφxABCψ
20 8 16 19 3bitr2d φφχθτφxABCψ
21 20 bianabs φφχθτxABCψ
22 21 bicomd φxABCψφχθτ
23 22 bianabs φxABCψχθτ