Proofgold Proof

pf

Let x0 of type ο be given.

Let x1 of type ο be given.

Let x2 of type ο be given.

Assume H0: iff x0 x1.

Assume H1: iff x1 x2.

Apply H0 with iff x0 x2.

Assume H2: x0 ⟶ x1.

Assume H3: x1 ⟶ x0.

Apply H1 with iff x0 x2.

Assume H4: x1 ⟶ x2.

Assume H5: x2 ⟶ x1.

Apply iffI with x0, x2 leaving 2 subgoals.

Assume H6: x0.

Apply H4.

Apply H2.

The subproof is completed by applying H6.

Assume H6: x2.

Apply H3.

Apply H5.

The subproof is completed by applying H6.

■