Metamath Proof Explorer


Definition df-had

Description: Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3, or testing whether an odd number of parameters are true). (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion df-had
|- ( hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph
 |-  ph
1 wps
 |-  ps
2 wch
 |-  ch
3 0 1 2 whad
 |-  hadd ( ph , ps , ch )
4 0 1 wxo
 |-  ( ph \/_ ps )
5 4 2 wxo
 |-  ( ( ph \/_ ps ) \/_ ch )
6 3 5 wb
 |-  ( hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )