Theorem and_or_absorbl ≪ | index | src | ≫

\and\or左吸收

theorem and_or_absorbl (A B: wff): $ A \and (A \or B) \iff A $;
StepHypRefExpression
1 iff_comp 
(\neg (A \imp \neg (\neg A \imp B)) \imp A) \imp (A \imp \neg (A \imp \neg (\neg A \imp B))) \imp (\neg (A \imp \neg (\neg A \imp B)) \iff A)
2 neg_imp_swap 
(\neg A \imp A \imp \neg (\neg A \imp B)) \imp \neg (A \imp \neg (\neg A \imp B)) \imp A
3 neg_elimintror_imp 
\neg A \imp A \imp \neg (\neg A \imp B)
4 2, 3 ax_mp 
\neg (A \imp \neg (\neg A \imp B)) \imp A
5 1, 4 ax_mp 
(A \imp \neg (A \imp \neg (\neg A \imp B))) \imp (\neg (A \imp \neg (\neg A \imp B)) \iff A)
6 imp_neg_swap 
((A \imp \neg (\neg A \imp B)) \imp \neg A) \imp A \imp \neg (A \imp \neg (\neg A \imp B))
7 imp_tran 
((A \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp \neg A) \imp (((\neg A \imp B) \imp \neg A) \imp \neg A) \imp (A \imp \neg (\neg A \imp B)) \imp \neg A
8 imp_neg_swap 
(A \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp \neg A
9 7, 8 ax_mp 
(((\neg A \imp B) \imp \neg A) \imp \neg A) \imp (A \imp \neg (\neg A \imp B)) \imp \neg A
10 imp_tran 
(((\neg A \imp B) \imp \neg A) \imp A \imp \neg A) \imp ((A \imp \neg A) \imp \neg A) \imp ((\neg A \imp B) \imp \neg A) \imp \neg A
11 imp_introrevr_imp 
(A \imp \neg A \imp B) \imp ((\neg A \imp B) \imp \neg A) \imp A \imp \neg A
12 intror_neg_imp 
A \imp \neg A \imp B
13 11, 12 ax_mp 
((\neg A \imp B) \imp \neg A) \imp A \imp \neg A
14 10, 13 ax_mp 
((A \imp \neg A) \imp \neg A) \imp ((\neg A \imp B) \imp \neg A) \imp \neg A
15 imp_neg_tosame_neg 
(A \imp \neg A) \imp \neg A
16 14, 15 ax_mp 
((\neg A \imp B) \imp \neg A) \imp \neg A
17 9, 16 ax_mp 
(A \imp \neg (\neg A \imp B)) \imp \neg A
18 6, 17 ax_mp 
A \imp \neg (A \imp \neg (\neg A \imp B))
19 5, 18 ax_mp 
\neg (A \imp \neg (\neg A \imp B)) \iff A
20 19 conv or 
\neg (A \imp \neg (A \or B)) \iff A
21 20 conv and 
A \and (A \or B) \iff A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)