Metamath Proof Explorer


Definition df-cgr3

Description: The three place congruence predicate. This is an abbreviation for saying that all three pair in a triple are congruent with each other. Three place form of Definition 4.4 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion df-cgr3 Cgr3=pq|na𝔼nb𝔼nc𝔼nd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccgr3 classCgr3
1 vp setvarp
2 vq setvarq
3 vn setvarn
4 cn class
5 va setvara
6 cee class𝔼
7 3 cv setvarn
8 7 6 cfv class𝔼n
9 vb setvarb
10 vc setvarc
11 vd setvard
12 ve setvare
13 vf setvarf
14 1 cv setvarp
15 5 cv setvara
16 9 cv setvarb
17 10 cv setvarc
18 16 17 cop classbc
19 15 18 cop classabc
20 14 19 wceq wffp=abc
21 2 cv setvarq
22 11 cv setvard
23 12 cv setvare
24 13 cv setvarf
25 23 24 cop classef
26 22 25 cop classdef
27 21 26 wceq wffq=def
28 15 16 cop classab
29 ccgr classCgr
30 22 23 cop classde
31 28 30 29 wbr wffabCgrde
32 15 17 cop classac
33 22 24 cop classdf
34 32 33 29 wbr wffacCgrdf
35 18 25 29 wbr wffbcCgref
36 31 34 35 w3a wffabCgrdeacCgrdfbcCgref
37 20 27 36 w3a wffp=abcq=defabCgrdeacCgrdfbcCgref
38 37 13 8 wrex wfff𝔼np=abcq=defabCgrdeacCgrdfbcCgref
39 38 12 8 wrex wffe𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref
40 39 11 8 wrex wffd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref
41 40 10 8 wrex wffc𝔼nd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref
42 41 9 8 wrex wffb𝔼nc𝔼nd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref
43 42 5 8 wrex wffa𝔼nb𝔼nc𝔼nd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref
44 43 3 4 wrex wffna𝔼nb𝔼nc𝔼nd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref
45 44 1 2 copab classpq|na𝔼nb𝔼nc𝔼nd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref
46 0 45 wceq wffCgr3=pq|na𝔼nb𝔼nc𝔼nd𝔼ne𝔼nf𝔼np=abcq=defabCgrdeacCgrdfbcCgref