Theorem wl-df4-3mintru2

Description: An alternative definition of the adder carry. Copy of df-cad . (Contributed by Mario Carneiro, 4-Sep-2016) df-cad redefined. (Revised by Wolf Lammen, 19-Jun-2024)

	Ref	Expression
Assertion	wl-df4-3mintru2	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		3orass	|- ( ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
2		wl-df2-3mintru2	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) )
3		xor2	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
4	3	biancomi	|- ( ( ph \/_ ps ) <-> ( -. ( ph /\ ps ) /\ ( ph \/ ps ) ) )
5	4	anbi1ci	|- ( ( ch /\ ( ph \/_ ps ) ) <-> ( ( -. ( ph /\ ps ) /\ ( ph \/ ps ) ) /\ ch ) )
6		anass	|- ( ( ( -. ( ph /\ ps ) /\ ( ph \/ ps ) ) /\ ch ) <-> ( -. ( ph /\ ps ) /\ ( ( ph \/ ps ) /\ ch ) ) )
7	5 6	bitri	|- ( ( ch /\ ( ph \/_ ps ) ) <-> ( -. ( ph /\ ps ) /\ ( ( ph \/ ps ) /\ ch ) ) )
8	7	orbi2i	|- ( ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) <-> ( ( ph /\ ps ) \/ ( -. ( ph /\ ps ) /\ ( ( ph \/ ps ) /\ ch ) ) ) )
9		pm5.63	|- ( ( ( ph /\ ps ) \/ ( ( ph \/ ps ) /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( -. ( ph /\ ps ) /\ ( ( ph \/ ps ) /\ ch ) ) ) )
10		andir	|- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )
11	10	orbi2i	|- ( ( ( ph /\ ps ) \/ ( ( ph \/ ps ) /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
12	8 9 11	3bitr2i	|- ( ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( ps /\ ch ) ) ) )
13	1 2 12	3bitr4i	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )