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 ( 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 ) ) )