Theorem cad1 1398

Description: If one parameter is true, the adder carry is true exactly when at least one of the other parameters is true. (Contributed by Mario Carneiro, 8-Sep-2016.)

Assertion

Ref	Expression
cad1	⊢ (χ → (cadd(φ, ψ, χ) ↔ (φ ∨ ψ)))

Proof of Theorem cad1

Step	Hyp	Ref	Expression
1		ibar 490	. . . 4 ⊢ (χ → ((φ ⊻ ψ) ↔ (χ ∧ (φ ⊻ ψ))))
2	1	bicomd 192	. . 3 ⊢ (χ → ((χ ∧ (φ ⊻ ψ)) ↔ (φ ⊻ ψ)))
3	2	orbi2d 682	. 2 ⊢ (χ → (((φ ∧ ψ) ∨ (χ ∧ (φ ⊻ ψ))) ↔ ((φ ∧ ψ) ∨ (φ ⊻ ψ))))
4		df-cad 1381	. 2 ⊢ (cadd(φ, ψ, χ) ↔ ((φ ∧ ψ) ∨ (χ ∧ (φ ⊻ ψ))))
5		pm5.63 890	. . 3 ⊢ (((φ ∧ ψ) ∨ (φ ∨ ψ)) ↔ ((φ ∧ ψ) ∨ (¬ (φ ∧ ψ) ∧ (φ ∨ ψ))))
6		olc 373	. . . 4 ⊢ ((φ ∨ ψ) → ((φ ∧ ψ) ∨ (φ ∨ ψ)))
7		orc 374	. . . . . 6 ⊢ (φ → (φ ∨ ψ))
8	7	adantr 451	. . . . 5 ⊢ ((φ ∧ ψ) → (φ ∨ ψ))
9		id 19	. . . . 5 ⊢ ((φ ∨ ψ) → (φ ∨ ψ))
10	8, 9	jaoi 368	. . . 4 ⊢ (((φ ∧ ψ) ∨ (φ ∨ ψ)) → (φ ∨ ψ))
11	6, 10	impbii 180	. . 3 ⊢ ((φ ∨ ψ) ↔ ((φ ∧ ψ) ∨ (φ ∨ ψ)))
12		xor2 1310	. . . . 5 ⊢ ((φ ⊻ ψ) ↔ ((φ ∨ ψ) ∧ ¬ (φ ∧ ψ)))
13		ancom 437	. . . . 5 ⊢ (((φ ∨ ψ) ∧ ¬ (φ ∧ ψ)) ↔ (¬ (φ ∧ ψ) ∧ (φ ∨ ψ)))
14	12, 13	bitri 240	. . . 4 ⊢ ((φ ⊻ ψ) ↔ (¬ (φ ∧ ψ) ∧ (φ ∨ ψ)))
15	14	orbi2i 505	. . 3 ⊢ (((φ ∧ ψ) ∨ (φ ⊻ ψ)) ↔ ((φ ∧ ψ) ∨ (¬ (φ ∧ ψ) ∧ (φ ∨ ψ))))
16	5, 11, 15	3bitr4i 268	. 2 ⊢ ((φ ∨ ψ) ↔ ((φ ∧ ψ) ∨ (φ ⊻ ψ)))
17	3, 4, 16	3bitr4g 279	1 ⊢ (χ → (cadd(φ, ψ, χ) ↔ (φ ∨ ψ)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ⊻ wxo 1304  caddwcad 1379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is used by: (None)