Metamath Proof Explorer


Theorem cad1

Description: If one input is true, then the adder carry is true exactly when at least one of the other two inputs is true. (Contributed by Mario Carneiro, 8-Sep-2016) (Proof shortened by Wolf Lammen, 19-Jun-2020)

Ref Expression
Assertion cad1
|- ( ch -> ( cadd ( ph , ps , ch ) <-> ( ph \/ ps ) ) )

Proof

Step Hyp Ref Expression
1 cadan
 |-  ( cadd ( ph , ps , ch ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) )
2 3anass
 |-  ( ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) <-> ( ( ph \/ ps ) /\ ( ( ph \/ ch ) /\ ( ps \/ ch ) ) ) )
3 1 2 bitri
 |-  ( cadd ( ph , ps , ch ) <-> ( ( ph \/ ps ) /\ ( ( ph \/ ch ) /\ ( ps \/ ch ) ) ) )
4 olc
 |-  ( ch -> ( ph \/ ch ) )
5 olc
 |-  ( ch -> ( ps \/ ch ) )
6 4 5 jca
 |-  ( ch -> ( ( ph \/ ch ) /\ ( ps \/ ch ) ) )
7 6 biantrud
 |-  ( ch -> ( ( ph \/ ps ) <-> ( ( ph \/ ps ) /\ ( ( ph \/ ch ) /\ ( ps \/ ch ) ) ) ) )
8 3 7 bitr4id
 |-  ( ch -> ( cadd ( ph , ps , ch ) <-> ( ph \/ ps ) ) )