A∨B⊢A∨(¬A∧B)

table:A∨B⊢A∨(¬A∧B)

前提番号 行番号 論理式 推論規則

1 1 A∨B 仮定

2 2 A 仮定

2 3 A∨(¬A∧B) 2,∨導入

4 4 B 仮定

5 A∨¬A 排中律

6 6 A 仮定

6 7 A∨(¬A∧B) 5,∨導入

8 8 ¬A 仮定

4,8 9 ¬A∧B 4,7,∧導入

4,8 10 A∨(¬A∧B) 8,∨導入

8 11 A∨(¬A∧B) 5-10,∨除去

1 12 A∨(¬A∧B) 1-11,∨除去

逆の証明