Known ax_mp^ax_mp : ∀ x0 x1 : ο . x0 ⟶ (x0 ⟶ x1) ⟶ x1
Known ax_frege52c^ax_frege52c : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ο . ∀ x3 . wceq (x1 x3) (x2 x3) ⟶ wsbc x0 (x1 x3) ⟶ wsbc x0 (x2 x3)
Known ax_frege8^ax_frege8 : ∀ x0 x1 x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x1 ⟶ x0 ⟶ x2
Theorem 24ac9..^frege53c : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ο . ∀ x3 . wsbc x0 (x1 x3) ⟶ wceq (x1 x3) (x2 x3) ⟶ wsbc x0 (x2 x3) (proof)

Proofgold Address