Theorem cadcoma 1395

Description: Commutative law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)

Assertion

Ref	Expression
cadcoma	⊢ (cadd(φ, ψ, χ) ↔ cadd(ψ, φ, χ))

Proof of Theorem cadcoma

Step	Hyp	Ref	Expression
1		ancom 437	. . 3 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ))
2		xorcom 1307	. . . 4 ⊢ ((φ ⊻ ψ) ↔ (ψ ⊻ φ))
3	2	anbi2i 675	. . 3 ⊢ ((χ ∧ (φ ⊻ ψ)) ↔ (χ ∧ (ψ ⊻ φ)))
4	1, 3	orbi12i 507	. 2 ⊢ (((φ ∧ ψ) ∨ (χ ∧ (φ ⊻ ψ))) ↔ ((ψ ∧ φ) ∨ (χ ∧ (ψ ⊻ φ))))
5		df-cad 1381	. 2 ⊢ (cadd(φ, ψ, χ) ↔ ((φ ∧ ψ) ∨ (χ ∧ (φ ⊻ ψ))))
6		df-cad 1381	. 2 ⊢ (cadd(ψ, φ, χ) ↔ ((ψ ∧ φ) ∨ (χ ∧ (ψ ⊻ φ))))
7	4, 5, 6	3bitr4i 268	1 ⊢ (cadd(φ, ψ, χ) ↔ cadd(ψ, φ, χ))

Syntax hints:   ↔ wb 176   ∨ wo 357   ∧ wa 358   ⊻ wxo 1304  caddwcad 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-xor 1305  df-cad 1381

This theorem is referenced by:  cadrot  1397