Theorem cadan

Description: The adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 25-Sep-2018)

	Ref	Expression
Assertion	cadan	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-3or	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
2		cador	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
3		andi	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) )
4	3	orbi1i	⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
5	1 2 4	3bitr4i	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
6		ordir	⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ∧ ( ( 𝜓 ∨ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ) )
7		ordi	⊢ ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) )
8		orcom	⊢ ( ( ( 𝜓 ∨ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∨ ( 𝜓 ∨ 𝜒 ) ) )
9		animorl	⊢ ( ( 𝜓 ∧ 𝜒 ) → ( 𝜓 ∨ 𝜒 ) )
10		pm4.72	⊢ ( ( ( 𝜓 ∧ 𝜒 ) → ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∨ ( 𝜓 ∨ 𝜒 ) ) ) )
11	9 10	mpbi	⊢ ( ( 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∨ ( 𝜓 ∨ 𝜒 ) ) )
12	8 11	bitr4i	⊢ ( ( ( 𝜓 ∨ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜓 ∨ 𝜒 ) )
13	7 12	anbi12i	⊢ ( ( ( 𝜑 ∨ ( 𝜓 ∧ 𝜒 ) ) ∧ ( ( 𝜓 ∨ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
14	5 6 13	3bitri	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
15		df-3an	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
16	14 15	bitr4i	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) )