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 ( ph , ps , ch ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-3or	|- ( ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( ps /\ ch ) ) )
2		cador	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) )
3		andi	|- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
4	3	orbi1i	|- ( ( ( ph /\ ( ps \/ ch ) ) \/ ( ps /\ ch ) ) <-> ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( ps /\ ch ) ) )
5	1 2 4	3bitr4i	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ( ps \/ ch ) ) \/ ( ps /\ ch ) ) )
6		ordir	|- ( ( ( ph /\ ( ps \/ ch ) ) \/ ( ps /\ ch ) ) <-> ( ( ph \/ ( ps /\ ch ) ) /\ ( ( ps \/ ch ) \/ ( ps /\ ch ) ) ) )
7		ordi	|- ( ( ph \/ ( ps /\ ch ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) ) )
8		orcom	|- ( ( ( ps \/ ch ) \/ ( ps /\ ch ) ) <-> ( ( ps /\ ch ) \/ ( ps \/ ch ) ) )
9		animorl	|- ( ( ps /\ ch ) -> ( ps \/ ch ) )
10		pm4.72	|- ( ( ( ps /\ ch ) -> ( ps \/ ch ) ) <-> ( ( ps \/ ch ) <-> ( ( ps /\ ch ) \/ ( ps \/ ch ) ) ) )
11	9 10	mpbi	|- ( ( ps \/ ch ) <-> ( ( ps /\ ch ) \/ ( ps \/ ch ) ) )
12	8 11	bitr4i	|- ( ( ( ps \/ ch ) \/ ( ps /\ ch ) ) <-> ( ps \/ ch ) )
13	7 12	anbi12i	|- ( ( ( ph \/ ( ps /\ ch ) ) /\ ( ( ps \/ ch ) \/ ( ps /\ ch ) ) ) <-> ( ( ( ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ps \/ ch ) ) )
14	5 6 13	3bitri	|- ( cadd ( ph , ps , ch ) <-> ( ( ( ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ps \/ ch ) ) )
15		df-3an	|- ( ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) <-> ( ( ( ph \/ ps ) /\ ( ph \/ ch ) ) /\ ( ps \/ ch ) ) )
16	14 15	bitr4i	|- ( cadd ( ph , ps , ch ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) )