Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply and3I with
reflexive (3897e.. x0 x1 x2),
symmetric (3897e.. x0 x1 x2),
transitive (3897e.. x0 x1 x2) leaving 3 subgoals.
The subproof is completed by applying unknownprop_f30a9971af522a7c6d48fce7503318aee70245a8fb07686f8a91c05461df8720 with x0, x1, x2.
The subproof is completed by applying unknownprop_6fd31505fe5649eb2fd16580ea5d6e63ee118f3692b3972694e2469c77d587b4 with x0, x1, x2.
The subproof is completed by applying unknownprop_b31e8bac4af8c42397918a9262a41224a434d0e78fc6fb9245dfb70f3b90add1 with x0, x1, x2.