Apply ax_mp__ax_1__ax_2__ax_3__df_bi__df_or__df_an__df_ifp__df_3or__df_3an__df_nan__df_xor__df_tru__df_fal__df_had__df_cad__df_ex__df_nf with
∀ x0 x1 : ο . x0 ⟶ x1 ⟶ x0.
Assume H0: ∀ x0 x1 : ο . x0 ⟶ (x0 ⟶ x1) ⟶ x1.
Assume H1: ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ x0.
Assume H2: ∀ x0 x1 x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ (x0 ⟶ x1) ⟶ x0 ⟶ x2.
Assume H3:
∀ x0 x1 : ο . (wn x0 ⟶ wn x1) ⟶ x1 ⟶ x0.
Assume H4:
∀ x0 x1 : ο . wn ((wb x0 x1 ⟶ wn ((x0 ⟶ x1) ⟶ wn (x1 ⟶ x0))) ⟶ wn (wn ((x0 ⟶ x1) ⟶ wn (x1 ⟶ x0)) ⟶ wb x0 x1)).
Assume H5:
∀ x0 x1 : ο . wb (wo x0 x1) (wn x0 ⟶ x1).
Assume H6:
∀ x0 x1 : ο . wb (wa x0 x1) (wn (x0 ⟶ wn x1)).
Assume H7:
∀ x0 x1 x2 : ο . wb (wif x0 x1 x2) (wo (wa x0 x1) (wa (wn x0) x2)).
Assume H8:
∀ x0 x1 x2 : ο . wb (w3o x0 x1 x2) (wo (wo x0 x1) x2).
Assume H9:
∀ x0 x1 x2 : ο . wb (w3a x0 x1 x2) (wa (wa x0 x1) x2).
Assume H10:
∀ x0 x1 : ο . wb (wnan x0 x1) (wn (wa x0 x1)).
Assume H11:
∀ x0 x1 : ο . wb (wxo x0 x1) (wn (wb x0 x1)).
Assume H14:
∀ x0 x1 x2 : ο . wb (whad x0 x1 x2) (wxo (wxo x0 x1) x2).
Assume H15:
∀ x0 x1 x2 : ο . wb (wcad x0 x1 x2) (wo (wa x0 x1) (wa x2 (wxo x0 x1))).
Assume H16:
∀ x0 : ι → ο . wb (wex (λ x1 . x0 x1)) (wn (∀ x1 . wn (x0 x1))).
Assume H17:
∀ x0 : ι → ο . wb (wnf (λ x1 . x0 x1)) (wex (λ x1 . x0 x1) ⟶ ∀ x1 . x0 x1).
The subproof is completed by applying H1.