Theorem or_and_absorbl ≪ | index | src | ≫

\or\and左吸收

theorem or_and_absorbl (A B: wff): $ A \or (A \and B) \iff A $;
StepHypRefExpression
1 iff_comp 
((\neg A \imp \neg (A \imp \neg B)) \imp A) \imp (A \imp \neg A \imp \neg (A \imp \neg B)) \imp (\neg A \imp \neg (A \imp \neg B) \iff A)
2 imp_tran 
((\neg A \imp \neg (A \imp \neg B)) \imp (A \imp \neg B) \imp A) \imp (((A \imp \neg B) \imp A) \imp A) \imp (\neg A \imp \neg (A \imp \neg B)) \imp A
3 neg_imp_elimrev 
(\neg A \imp \neg (A \imp \neg B)) \imp (A \imp \neg B) \imp A
4 2, 3 ax_mp 
(((A \imp \neg B) \imp A) \imp A) \imp (\neg A \imp \neg (A \imp \neg B)) \imp A
5 imp_tran 
(((A \imp \neg B) \imp A) \imp \neg A \imp A) \imp ((\neg A \imp A) \imp A) \imp ((A \imp \neg B) \imp A) \imp A
6 imp_introrevr_imp 
(\neg A \imp A \imp \neg B) \imp ((A \imp \neg B) \imp A) \imp \neg A \imp A
7 neg_elimintror_imp 
\neg A \imp A \imp \neg B
8 6, 7 ax_mp 
((A \imp \neg B) \imp A) \imp \neg A \imp A
9 5, 8 ax_mp 
((\neg A \imp A) \imp A) \imp ((A \imp \neg B) \imp A) \imp A
10 neg_imp_tosame 
(\neg A \imp A) \imp A
11 9, 10 ax_mp 
((A \imp \neg B) \imp A) \imp A
12 4, 11 ax_mp 
(\neg A \imp \neg (A \imp \neg B)) \imp A
13 1, 12 ax_mp 
(A \imp \neg A \imp \neg (A \imp \neg B)) \imp (\neg A \imp \neg (A \imp \neg B) \iff A)
14 intror_neg_imp 
A \imp \neg A \imp \neg (A \imp \neg B)
15 13, 14 ax_mp 
\neg A \imp \neg (A \imp \neg B) \iff A
16 15 conv or 
A \or \neg (A \imp \neg B) \iff A
17 16 conv and 
A \or (A \and B) \iff A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)