Metamath Proof Explorer


Theorem cadifp

Description: The value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs. (Contributed by BJ, 8-Oct-2019)

Ref Expression
Assertion cadifp ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( 𝜒 , ( 𝜑𝜓 ) , ( 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 cad1 ( 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
2 cad0 ( ¬ 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
3 1 2 casesifp ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( 𝜒 , ( 𝜑𝜓 ) , ( 𝜑𝜓 ) ) )