Let x0 of type ο be given.
Let x1 of type ο be given.
Let x2 of type ο be given.
Assume H3:
not x0 ⟶ or x1 x2.
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 H1 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Assume H5: x1.
Apply H2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
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 H0.
Apply H3 with
x1 leaving 3 subgoals.
The subproof is completed by applying H5.
Assume H6: x1.
The subproof is completed by applying H6.
Assume H6: x2.
Apply H4 with
x1.
The subproof is completed by applying H6.
The subproof is completed by applying H4.