Proofgold Address

Known not_def^not_def : not = λ x1 : ο . x1 ⟶ False
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0 (proof)
Known and_def^and_def : and = λ x1 x2 : ο . ∀ x3 : ο . (x1 ⟶ x2 ⟶ x3) ⟶ x3
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1 (proof)
Known f13f4..^or_def : or = λ x1 x2 : ο . ∀ x3 : ο . (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Theorem 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2 (proof)
Theorem dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1 (proof)
Theorem eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1 (proof)
Known 5f92b..^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem 9ac15..^xm : ∀ x0 : ο . or x0 (not x0) (proof)
Theorem 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1 (proof)
Known 13bcd..^iff_def : iff = λ x1 x2 : ο . and (x1 ⟶ x2) (x2 ⟶ x1)
Theorem d182e..^iffE : ∀ x0 x1 : ο . iff x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ (not x0 ⟶ not x1 ⟶ x2) ⟶ x2 (proof)
Theorem 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1 (proof)