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 ( ph , ps , ch ) <-> if- ( ph , ( ps <-> ch ) , ( ps \/_ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		had1	|- ( ph -> ( hadd ( ph , ps , ch ) <-> ( ps <-> ch ) ) )
2		had0	|- ( -. ph -> ( hadd ( ph , ps , ch ) <-> ( ps \/_ ch ) ) )
3	1 2	casesifp	|- ( hadd ( ph , ps , ch ) <-> if- ( ph , ( ps <-> ch ) , ( ps \/_ ch ) ) )