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 ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		3orass	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ) )
2		wl-df2-3mintru2	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
3		xor2	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ¬ ( 𝜑 ∧ 𝜓 ) ) )
4	3	biancomi	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∨ 𝜓 ) ) )
5	4	anbi1ci	⊢ ( ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ↔ ( ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∨ 𝜓 ) ) ∧ 𝜒 ) )
6		anass	⊢ ( ( ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∨ 𝜓 ) ) ∧ 𝜒 ) ↔ ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ) )
7	5 6	bitri	⊢ ( ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ↔ ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ) )
8	7	orbi2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ) ) )
9		pm5.63	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ ( 𝜑 ∧ 𝜓 ) ∧ ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ) ) )
10		andir	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
11	10	orbi2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ) )
12	8 9 11	3bitr2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ) )
13	1 2 12	3bitr4i	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) )