Proofgold Asset

Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 91bfe..^dnegI : ∀ x0 : ο . x0 ⟶ not (not x0) (proof)
Known 5f92b..^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0 (proof)
Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Theorem 0a8dd..^keepcopy : ∀ x0 : ο . (not x0 ⟶ x0) ⟶ x0 (proof)
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 3f786..^orI_contra : ∀ x0 x1 : ο . (not x0 ⟶ not x1 ⟶ False) ⟶ or x0 x1 (proof)
Theorem d47b4..^orI_imp1 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ or (not x0) x1 (proof)
Theorem d5b81..^orI_imp2 : ∀ x0 x1 : ο . (x1 ⟶ x0) ⟶ or x0 (not x1) (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 57def..^tab_pos_and : ∀ x0 x1 : ο . and x0 x1 ⟶ (x0 ⟶ x1 ⟶ False) ⟶ False (proof)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem 26b88..^tab_pos_or : ∀ x0 x1 : ο . or x0 x1 ⟶ (x0 ⟶ False) ⟶ (x1 ⟶ False) ⟶ False (proof)
Theorem 7ffa0..^tab_pos_imp : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ False) ⟶ (x1 ⟶ False) ⟶ False (proof)
Known d182e..^iffE : ∀ x0 x1 : ο . iff x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ (not x0 ⟶ not x1 ⟶ x2) ⟶ x2
Theorem a19af..^tab_pos_iff : ∀ x0 x1 : ο . iff x0 x1 ⟶ (x0 ⟶ x1 ⟶ False) ⟶ (not x0 ⟶ not x1 ⟶ False) ⟶ False (proof)
Theorem c44ec..^tab_neg_imp : ∀ x0 x1 : ο . not (x0 ⟶ x1) ⟶ (x0 ⟶ not x1 ⟶ False) ⟶ False (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 77eb0..^tab_neg_and : ∀ x0 x1 : ο . not (and x0 x1) ⟶ (not x0 ⟶ False) ⟶ (not x1 ⟶ False) ⟶ False (proof)
Theorem 6a5f4..^tab_neg_or : ∀ x0 x1 : ο . not (or x0 x1) ⟶ (not x0 ⟶ not x1 ⟶ False) ⟶ False (proof)
Known 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem b2d9e..^tab_neg_iff : ∀ x0 x1 : ο . not (iff x0 x1) ⟶ (x0 ⟶ not x1 ⟶ False) ⟶ (not x0 ⟶ x1 ⟶ False) ⟶ False (proof)
Known 2540e..^prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Theorem prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1 (proof)
Theorem 30c0c..^eqo_iff : ∀ x0 x1 : ο . x0 = x1 ⟶ iff x0 x1 (proof)
Theorem d0d7f..^tab_pos_eqo : ∀ x0 x1 : ο . x0 = x1 ⟶ (x0 ⟶ x1 ⟶ False) ⟶ (not x0 ⟶ not x1 ⟶ False) ⟶ False (proof)
Theorem 7a33c..^tab_neg_eqo : ∀ x0 x1 : ο . not (x0 = x1) ⟶ (x0 ⟶ not x1 ⟶ False) ⟶ (not x0 ⟶ x1 ⟶ False) ⟶ False (proof)
Theorem b4c6f..^{tab_pos_all_i} : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ (x0 x1 ⟶ False) ⟶ False (proof)
Theorem 29614..^{tab_neg_all_i} : ∀ x0 : ι → ο . not (∀ x1 . x0 x1) ⟶ (∀ x1 . not (x0 x1) ⟶ False) ⟶ False (proof)
Theorem 2f8d2..^tab_pos_ex_i : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 . x0 x1 ⟶ False) ⟶ False (proof)
Theorem 2f8d2..^tab_pos_ex_i : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 . x0 x1 ⟶ False) ⟶ False (proof)
Theorem 18cb3..^tab_mat_i_o : ∀ x0 : ι → ο . ∀ x1 x2 . x0 x1 ⟶ not (x0 x2) ⟶ (not (x1 = x2) ⟶ False) ⟶ False (proof)
Theorem 8c503..^{tab_mat_i_i_o} : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 x4 . x0 x1 x2 ⟶ not (x0 x3 x4) ⟶ (not (x1 = x3) ⟶ False) ⟶ (not (x2 = x4) ⟶ False) ⟶ False (proof)
Theorem 2b3a3..^tab_confront : ∀ x0 x1 x2 x3 . x0 = x1 ⟶ not (x2 = x3) ⟶ (not (x0 = x2) ⟶ not (x1 = x2) ⟶ False) ⟶ (not (x0 = x3) ⟶ not (x1 = x3) ⟶ False) ⟶ False (proof)
Theorem f_eq_i^f_equal_i_i : ∀ x0 : ι → ι . ∀ x1 x2 . x1 = x2 ⟶ x0 x1 = x0 x2 (proof)
Theorem 31719..^tab_dec_i : ∀ x0 : ι → ι . ∀ x1 x2 . not (x0 x1 = x0 x2) ⟶ (not (x1 = x2) ⟶ False) ⟶ False (proof)
Theorem f_eq_i_i^{f_equal_i_i_i} : ∀ x0 : ι → ι → ι . ∀ x1 x2 x3 x4 . x1 = x2 ⟶ x3 = x4 ⟶ x0 x1 x3 = x0 x2 x4 (proof)
Theorem 06083..^tab_dec_i_i : ∀ x0 : ι → ι → ι . ∀ x1 x2 x3 x4 . not (x0 x1 x3 = x0 x2 x4) ⟶ (not (x1 = x2) ⟶ False) ⟶ (not (x3 = x4) ⟶ False) ⟶ False (proof)
Theorem 3f27c..^{tab_pos_eqf_i_i} : ∀ x0 x1 : ι → ι . ∀ x2 . x0 = x1 ⟶ (x0 x2 = x1 x2 ⟶ False) ⟶ False (proof)
Theorem 48643..^{tab_pos_neqf_i_i} : ∀ x0 x1 : ι → ι . not (x0 = x1) ⟶ (∀ x2 . not (x0 x2 = x1 x2) ⟶ False) ⟶ False (proof)