Theorem cadcomb

Description: Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

	Ref	Expression
Assertion	cadcomb	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ cadd ( 𝜑 , 𝜒 , 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		cadan	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
2		3ancoma	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜓 ∨ 𝜒 ) ) )
3		orcom	⊢ ( ( 𝜓 ∨ 𝜒 ) ↔ ( 𝜒 ∨ 𝜓 ) )
4	3	3anbi3i	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜒 ∨ 𝜓 ) ) )
5	1 2 4	3bitri	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜒 ∨ 𝜓 ) ) )
6		cadan	⊢ ( cadd ( 𝜑 , 𝜒 , 𝜓 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜓 ) ∧ ( 𝜒 ∨ 𝜓 ) ) )
7	5 6	bitr4i	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ cadd ( 𝜑 , 𝜒 , 𝜓 ) )