Proofgold Address

Known 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 : ∀ x0 : ο . ((∀ x1 x2 : ο . x1 ⟶ (x1 ⟶ x2) ⟶ x2) ⟶ (∀ x1 x2 : ο . x1 ⟶ x2 ⟶ x1) ⟶ (∀ x1 x2 x3 : ο . (x1 ⟶ x2 ⟶ x3) ⟶ (x1 ⟶ x2) ⟶ x1 ⟶ x3) ⟶ (∀ x1 x2 : ο . (wn x1 ⟶ wn x2) ⟶ x2 ⟶ x1) ⟶ (∀ x1 x2 : ο . wn ((wb x1 x2 ⟶ wn ((x1 ⟶ x2) ⟶ wn (x2 ⟶ x1))) ⟶ wn (wn ((x1 ⟶ x2) ⟶ wn (x2 ⟶ x1)) ⟶ wb x1 x2))) ⟶ (∀ x1 x2 : ο . wb (wo x1 x2) (wn x1 ⟶ x2)) ⟶ (∀ x1 x2 : ο . wb (wa x1 x2) (wn (x1 ⟶ wn x2))) ⟶ (∀ x1 x2 x3 : ο . wb (wif x1 x2 x3) (wo (wa x1 x2) (wa (wn x1) x3))) ⟶ (∀ x1 x2 x3 : ο . wb (w3o x1 x2 x3) (wo (wo x1 x2) x3)) ⟶ (∀ x1 x2 x3 : ο . wb (w3a x1 x2 x3) (wa (wa x1 x2) x3)) ⟶ (∀ x1 x2 : ο . wb (wnan x1 x2) (wn (wa x1 x2))) ⟶ (∀ x1 x2 : ο . wb (wxo x1 x2) (wn (wb x1 x2))) ⟶ wb wtru ((∀ x1 . wceq (cv x1) (cv x1)) ⟶ ∀ x1 . wceq (cv x1) (cv x1)) ⟶ wb wfal (wn wtru) ⟶ (∀ x1 x2 x3 : ο . wb (whad x1 x2 x3) (wxo (wxo x1 x2) x3)) ⟶ (∀ x1 x2 x3 : ο . wb (wcad x1 x2 x3) (wo (wa x1 x2) (wa x3 (wxo x1 x2)))) ⟶ (∀ x1 : ι → ο . wb (wex x1) (wn (∀ x2 . wn (x1 x2)))) ⟶ (∀ x1 : ι → ο . wb (wnf x1) (wex x1 ⟶ ∀ x2 . x1 x2)) ⟶ x0) ⟶ x0
Theorem ax_mp^ax_mp : ∀ x0 x1 : ο . x0 ⟶ (x0 ⟶ x1) ⟶ x1
Theorem ax_frege1 : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ x0
Theorem ax_frege2 : ∀ x0 x1 x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ (x0 ⟶ x1) ⟶ x0 ⟶ x2
Theorem ax_3 : ∀ x0 x1 : ο . (wn x0 ⟶ wn x1) ⟶ x1 ⟶ x0
Theorem df_bi : ∀ x0 x1 : ο . wn ((wb x0 x1 ⟶ wn ((x0 ⟶ x1) ⟶ wn (x1 ⟶ x0))) ⟶ wn (wn ((x0 ⟶ x1) ⟶ wn (x1 ⟶ x0)) ⟶ wb x0 x1))
Theorem df_or : ∀ x0 x1 : ο . wb (wo x0 x1) (wn x0 ⟶ x1)
Theorem df_an : ∀ x0 x1 : ο . wb (wa x0 x1) (wn (x0 ⟶ wn x1))
Theorem df_ifp : ∀ x0 x1 x2 : ο . wb (wif x0 x1 x2) (wo (wa x0 x1) (wa (wn x0) x2))
Theorem df_3or : ∀ x0 x1 x2 : ο . wb (w3o x0 x1 x2) (wo (wo x0 x1) x2)
Theorem df_3an : ∀ x0 x1 x2 : ο . wb (w3a x0 x1 x2) (wa (wa x0 x1) x2)
Theorem df_nan : ∀ x0 x1 : ο . wb (wnan x0 x1) (wn (wa x0 x1))
Theorem df_xor : ∀ x0 x1 : ο . wb (wxo x0 x1) (wn (wb x0 x1))
Theorem df_tru : wb wtru ((∀ x0 . wceq (cv x0) (cv x0)) ⟶ ∀ x0 . wceq (cv x0) (cv x0))
Theorem df_fal : wb wfal (wn wtru)
Theorem df_had : ∀ x0 x1 x2 : ο . wb (whad x0 x1 x2) (wxo (wxo x0 x1) x2)
Theorem df_cad : ∀ x0 x1 x2 : ο . wb (wcad x0 x1 x2) (wo (wa x0 x1) (wa x2 (wxo x0 x1)))
Theorem df_ex : ∀ x0 : ι → ο . wb (wex x0) (wn (∀ x1 . wn (x0 x1)))
Theorem df_nf : ∀ x0 : ι → ο . wb (wnf x0) (wex x0 ⟶ ∀ x1 . x0 x1)