Metamath Proof Explorer


Theorem hadifp

Description: The value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs. (Contributed by BJ, 11-Aug-2020)

Ref Expression
Assertion hadifp ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( 𝜑 , ( 𝜓𝜒 ) , ( 𝜓𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 had1 ( 𝜑 → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜓𝜒 ) ) )
2 had0 ( ¬ 𝜑 → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜓𝜒 ) ) )
3 1 2 casesifp ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( 𝜑 , ( 𝜓𝜒 ) , ( 𝜓𝜒 ) ) )