Metamath Proof Explorer


Syntax definition whad

Description: Syntax for the "sum" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion whad wff hadd ( 𝜑 , 𝜓 , 𝜒 )