Proofgold Address

Known False_def^False_def : False = ∀ x1 : ο . x1
Known True_def^True_def : True = ∀ x1 : ο . x1 ⟶ x1
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 13bcd..^iff_def : iff = λ x1 x2 : ο . and (x1 ⟶ x2) (x2 ⟶ x1)
Known 2540e..^prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known 9ac15..^xm : ∀ x0 : ο . or x0 (not x0)
Theorem dd7e1.. : ∀ x0 : ο . or (x0 = True) (x0 = False) (proof)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem 06486.. : ∀ x0 x1 : ο . or x0 x1 ⟶ not x0 ⟶ x1 (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem e7295.. : ∀ x0 x1 : ο . x0 = x1 ⟶ and (x0 ⟶ x1) (x1 ⟶ x0) (proof)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem fcbcf..^{not_all_ex_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 . x0 x1) ⟶ ∀ x1 : ο . (∀ x2 . not (x0 x2) ⟶ x1) ⟶ x1 (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known 9ac15..^xm : ∀ x0 : ο . or x0 (not x0)
Theorem 35ec9.. : ∀ x0 x1 : ο . not (and x0 x1) ⟶ or (not x0) (not x1) (proof)
Theorem ee74e.. : ∀ x0 x1 : ο . not (or x0 x1) ⟶ and (not x0) (not x1) (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 13bcd..^iff_def : iff = λ x1 x2 : ο . and (x1 ⟶ x2) (x2 ⟶ x1)
Known 2540e..^prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Theorem 451e3.. : ∀ x0 x1 : ο . not (x0 = x1) ⟶ (x1 ⟶ x0) ⟶ not (x0 ⟶ x1) (proof)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Theorem 5f823..^{not_ex_all_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 . not (x0 x1) (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Theorem 0ff1b.. : ∀ x0 x1 : ο . not (x0 ⟶ x1) ⟶ and x0 (not x1) (proof)
Known 5f92b..^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem 5f92b..^dneg : ∀ x0 : ο . not (not x0) ⟶ x0 (proof)
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Theorem 91bfe..^dnegI : ∀ x0 : ο . x0 ⟶ not (not x0) (proof)
Theorem bc5df.. : ∀ x0 x1 : ο . (not x0 ⟶ not x1) ⟶ x1 ⟶ x0 (proof)
Theorem 0b2fd.. : ∀ x0 x1 : ο . (not x0 ⟶ x1) ⟶ not x1 ⟶ x0 (proof)
Theorem a5e64.. : ∀ x0 x1 : ο . (x0 ⟶ not x1) ⟶ x1 ⟶ not x0 (proof)
Theorem 5232a.. : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ not x1 ⟶ not x0 (proof)