Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 df-3or ( ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ∨ ( 𝜓𝜒 ) ) ↔ ( ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) ∨ ( 𝜓𝜒 ) ) )
2 cador ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ∨ ( 𝜓𝜒 ) ) )
3 andi ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) )
4 3 orbi1i ( ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) ∨ ( 𝜓𝜒 ) ) ↔ ( ( ( 𝜑𝜓 ) ∨ ( 𝜑𝜒 ) ) ∨ ( 𝜓𝜒 ) ) )
5 1 2 4 3bitr4i ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) ∨ ( 𝜓𝜒 ) ) )
6 ordir ( ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) ∨ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑 ∨ ( 𝜓𝜒 ) ) ∧ ( ( 𝜓𝜒 ) ∨ ( 𝜓𝜒 ) ) ) )
7 ordi ( ( 𝜑 ∨ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) )
8 orcom ( ( ( 𝜓𝜒 ) ∨ ( 𝜓𝜒 ) ) ↔ ( ( 𝜓𝜒 ) ∨ ( 𝜓𝜒 ) ) )
9 animorl ( ( 𝜓𝜒 ) → ( 𝜓𝜒 ) )
10 pm4.72 ( ( ( 𝜓𝜒 ) → ( 𝜓𝜒 ) ) ↔ ( ( 𝜓𝜒 ) ↔ ( ( 𝜓𝜒 ) ∨ ( 𝜓𝜒 ) ) ) )
11 9 10 mpbi ( ( 𝜓𝜒 ) ↔ ( ( 𝜓𝜒 ) ∨ ( 𝜓𝜒 ) ) )
12 8 11 bitr4i ( ( ( 𝜓𝜒 ) ∨ ( 𝜓𝜒 ) ) ↔ ( 𝜓𝜒 ) )
13 7 12 anbi12i ( ( ( 𝜑 ∨ ( 𝜓𝜒 ) ) ∧ ( ( 𝜓𝜒 ) ∨ ( 𝜓𝜒 ) ) ) ↔ ( ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) ∧ ( 𝜓𝜒 ) ) )
14 5 6 13 3bitri ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) ∧ ( 𝜓𝜒 ) ) )
15 df-3an ( ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ∧ ( 𝜓𝜒 ) ) ↔ ( ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ) ∧ ( 𝜓𝜒 ) ) )
16 14 15 bitr4i ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑𝜓 ) ∧ ( 𝜑𝜒 ) ∧ ( 𝜓𝜒 ) ) )