Let x0 of type ο be given.
Let x1 of type ο be given.
Let x2 of type ο be given.
Apply xm with
x2,
exactly1of3 x0 x1 x2 leaving 2 subgoals.
Assume H4: x2.
Apply orIR with
and (exactly1of2 x0 x1) (not x2),
and (and (not x0) (not x1)) x2.
Apply and3I with
not x0,
not x1,
x2 leaving 3 subgoals.
Assume H5: x0.
Apply H0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H5: x1.
Apply H1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Apply orIL with
and (exactly1of2 x0 x1) (not x2),
and (and (not x0) (not x1)) x2.
Apply andI with
exactly1of2 x0 x1,
not x2 leaving 2 subgoals.
Apply exactly1of2_impI1 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.