¬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,∨除去