Theorem cador

Description: The adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

	Ref	Expression
Assertion	cador	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		xor2	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
2	1	rbaib	|- ( -. ( ph /\ ps ) -> ( ( ph \/_ ps ) <-> ( ph \/ ps ) ) )
3	2	anbi1d	|- ( -. ( ph /\ ps ) -> ( ( ( ph \/_ ps ) /\ ch ) <-> ( ( ph \/ ps ) /\ ch ) ) )
4		ancom	|- ( ( ( ph \/_ ps ) /\ ch ) <-> ( ch /\ ( ph \/_ ps ) ) )
5		andir	|- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )
6	3 4 5	3bitr3g	|- ( -. ( ph /\ ps ) -> ( ( ch /\ ( ph \/_ ps ) ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
7	6	pm5.74i	|- ( ( -. ( ph /\ ps ) -> ( ch /\ ( ph \/_ ps ) ) ) <-> ( -. ( ph /\ ps ) -> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
8		df-or	|- ( ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) <-> ( -. ( ph /\ ps ) -> ( ch /\ ( ph \/_ ps ) ) ) )
9		df-or	|- ( ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) <-> ( -. ( ph /\ ps ) -> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
10	7 8 9	3bitr4i	|- ( ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
11		df-cad	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )
12		3orass	|- ( ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
13	10 11 12	3bitr4i	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) )